@inproceedings{libalf,
 author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker and Daniel Neider and David R. Piegdon},
 title = {libalf: The Automata Learning Framework},
 booktitle = {CAV},
 pages = {360-364},
 year = {2010},
 series = {LNCS},
 publisher = {Springer}
 }

@ARTICLE{learnlib,
  AUTHOR =       {Harald Raffelt and Bernhard Steffen and Therese Berg and Tiziana Margaria},
  TITLE =        {LearnLib: a framework for extrapolating behavioral models},
  JOURNAL =      {STTT},
  YEAR =         {2009},
  volume =       {11},
  number =       {5},
  pages =        {393-407}
}

@TECHREPORT{CW12,
  AUTHOR =       {Yu-Fang Chen and Bow-Yaw Wang},
  TITLE =        {Learning Boolean Function Increamentally},
  INSTITUTION =  {Academia Sinica},
  YEAR =         {2011},
  number =       {IIS-XXXX}
}


@inproceedings{JKWY:10:DIPL,
 author = {Yungbum Jung and Soonho Kong and Bow-Yaw Wang and Kwangkeun Yi},
 title = {Deriving Invariants in Propositional Logic by Algorithmic Learning,
          Decision Procedure, and Predicate Abstraction},
 editor    = {Gilles Barthe and Manuel V. Hermenegildo},
 booktitle = {VMCAI},
 pages = {180--196},
 year = {2010},
 series = {LNCS},
 publisher = {Springer},
 }

@inproceedings{KJDWI:10:AIQLI,
  author    = {Soonho Kong and Yungbum Jung and Cristina David and
                  Bow-Yaw Wang and Kwangkeun Yi},
  title     = {Automatically Inferring Quantified Loop Invariants by Algorithmic
               Learning from Simple Templates},
  booktitle = {APLAS},
  year      = {2010},
  pages     = {328-343},
  editor    = {Kazunori Ueda},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6461},
}

@inproceedings{JLWY:11:PGLBQFLII,
  author    = {Yungbum Jung and Wonchan Lee and Bow-Yaw Wang and
               Kwangkeun Yi},
  title     = {Predicate Generation for Learning-Based Quantifier-Free
               Loop Invariant Inference},
  year      = {2011},
  pages     = {205-219},
  editor    = {Parosh Aziz Abdulla and K. Rustan M. Leino},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6605},
}

@Article{a-lrsqc-87,
  author =       "D. Angluin",
  title =        "Learning Regular Sets from Queries and
                 Counterexamples",
  journal =      "Information and  Computation",
  volume =       "75",
  number =       "2",
  month =        nov,
  year =         "1987",
  pages =        "87--106",
  comment =      "Learning regular sets from a teacher who answers
                 membership queries, and responds to false conjectures
                 with counterexamples. Based on Gold's approach. Also
                 learning context-free languages from teacher. Was Yale
                 TR YALEU/DCS/TR-464",
}

@InProceedings{COLT::MalerP1991,
  title =        "On the Learnability of Infinitary Regular Sets",
  author =       "Oded Maler and Amir Pnueli",
  pages =        "128--136",
  booktitle =    "Proceedings of the Fourth Annual Workshop on
                 Computational Learning Theory",
  address =      "University of California, Santa Cruz",
  month =        "5--7~" # aug,
  year =         "1991",
  publisher =    "ACM Press",
}

@Book{KV:1994:ICLT,
  author =    "Michael J. Kearns and Umesh V. Vazirani",
  title =        "An Introduction to Computational Learning Theory",
  publisher =    "MIT Press",
  year =         "1994",
}

@inproceedings{FQ:02:PASV,
 author = {Cormac Flanagan and Shaz Qadeer},
 title = {Predicate abstraction for software verification},
 booktitle = {POPL},
 year = 2002,
 isbn = {1-58113-450-9},
 pages = {191--202},
 publisher = {ACM},
 }

@inproceedings{HV:05,
 author = {Peter Habermehl and Tomas Vojnar},
 title = {Regular Model Checking Using Inference of Regular Languages},
 booktitle = {ENTCS},
 year = 2005,
 pages = {21--36}
 }



@article{PR:07:TPAFT,
  author    = {Andreas Podelski and Andrey Rybalchenko},
  title     = {Transition predicate abstraction and fair termination},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {29},
  number    = {3},
  year      = {2007},
}

@inproceedings{CPR:05:ART,
  author    = {Byron Cook and Andreas Podelski and Andrey Rybalchenko},
  title     = {Abstraction Refinement for Termination},
  booktitle = {SAS},
  year      = {2005},
  pages     = {87-101},
  editor    = {Chris Hankin and Igor Siveroni},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3672},
}

@inproceedings{CPR:06:TPSC,
  author    = {Byron Cook and Andreas Podelski and Andrey Rybalchenko},
  title     = {Termination proofs for systems code},
  booktitle = {PLDI},
  year      = {2006},
  pages     = {415-426},
  editor    = {Michael I. Schwartzbach and Thomas Ball},
  publisher = {ACM},
}

@inproceedings{PR:05:TPAFT,
  author    = {Andreas Podelski and Andrey Rybalchenko},
  title     = {Transition predicate abstraction and fair termination},
  booktitle = {POPL},
  year      = {2005},
  pages     = {132-144},
  editor    = {Jens Palsberg and Mart\'{\i}n Abadi},
  publisher = {ACM},
}


@inproceedings{PR:04:TI,
  author    = {Andreas Podelski and Andrey Rybalchenko},
  title     = {Transition Invariants},
  booktitle = {LICS},
  year      = {2004},
  pages     = {32-41},
  publisher = {IEEE Computer Society},
  year      = {2004},
}

@inproceedings{PR:04:ACMSL,
  author    = {Andreas Podelski and Andrey Rybalchenko},
  title     = {A Complete Method for the Synthesis of Linear Ranking Functions},
  booktitle = {VMCAI},
  year      = {2004},
  pages     = {239-251},
  editor    = {Bernhard Steffen and Giorgio Levi},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2937},
}

@inproceedings{BHKL:09:ASLN,
  author    = {Benedikt Bollig and Peter Habermehl and Carsten Kern and
               Martin Leucker},
  title     = {Angluin-Style Learning of {NFA}},
  booktitle = {IJCAI},
  year      = {2009},
  pages     = {1004-1009},
  editor    = {Craig Boutilier},
}

@inproceedings{T:08:PPRMR,
  author    = {Laurent Th{\'e}ry},
  title     = {Proof Pearl: Revisiting the Mini-{Rubik} in {Coq}},
  booktitle = {TPHOLs},
  year      = 2008,
  pages     = {310-319},
  editor    = {Otmane A\"{\i}t Mohamed and
               C{\'e}sar Mu{\~n}oz and
               Sofi{\`e}ne Tahar},
  publisher = {Springer},
  series    = {LNCS},
  volume    = 5170,
}


@INPROCEEDINGS{KC:90:PACBDD,
author =      {S. Kimura and Edmund M. Clarke},
booktitle =   {ICCD},
title =       {A parallel algorithm for constructing binary decision diagrams},
year =        {1990},
pages =       {220-223},
publisher =   {IEEE Computer Society},
}

@Misc{CK:02:SEBP,
  author =    {Edmund M. Clarke and Daniel Kr{\"o}ning},
  title =     {{SMV} example: Bus protocol},
  year =      {2002},
  note =      {PowerPoint file},
}

@inproceedings{CCMM:95:VPPL,
  author    = {S{\'e}rgio Vale Aguiar Campos and Edmund M. Clarke and
               Wilfredo R. Marrero and Marius Minea},
  title     = {Verifying the performance of the {PCI} local bus using symbolic
               techniques},
  booktitle = {ICCD},
  year      = {1995},
  pages     = {72-78},
  publisher = {IEEE Computer Society},
}

@article{N:05:AEQLA,
  author    = {Atsuyoshi Nakamura},
  title     = {An efficient query learning algorithm for ordered binary
               decision diagrams},
  journal   = {Information and Computation},
  volume    = {201},
  number    = {2},
  year      = {2005},
  pages     = {178-198},
}


@inproceedings{GG:95:LOBDD,
  author    = {Ricard Gavald{\`a} and David Guijarro},
  title     = {Learning Ordered Binary Decision Diagrams},
  booktitle = {ALT},
  year      = {1995},
  pages     = {228-238},
  editor    = {Klaus P. Jantke and Takeshi Shinohara and Thomas Zeugmann},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {997},
}


@inproceedings{AV:10:LIOA,
  author    = {Fides Aarts and Frits W. Vaandrager},
  title     = {Learning {I/O} Automata},
  booktitle = {CONCUR},
  year      = {2010},
  pages     = {71-85},
  editor    = {Paul Gastin and Fran\c{c}ois Laroussinie},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6269},
}


@inproceedings{AJU:10:GMISCP,
  author    = {Fides Aarts and Bengt Jonsson and Johan Uijen},
  title     = {Generating Models of Infinite-State Communication Protocols
               Using Regular Inference with Abstraction},
  booktitle = {ICTSS},
  year      = {2010},
  pages     = {188-204},
  editor    = {Alexandre Petrenko and Adenilso da Silva Sim{\~a}o and
               Jos{\'e} Carlos Maldonado},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6435},
}



@inproceedings{SGP:10:LCIMMA,
  author    = {Rishabh Singh and Dimitra Giannakopoulou and
               Corina S. Pasareanu},
  title     = {Learning Component Interfaces with May and Must Abstractions},
  booktitle = {CAV},
  year      = {2010},
  pages     = {527-542},
  editor    = {Tayssir Touili and Byron Cook and Paul Jackson},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6174},
}


@inproceedings{BM:10:ABC,
  author    = {Robert K. Brayton and Alan Mishchenko},
  title     = {{ABC}: An Academic Industrial-Strength Verification Tool},
  booktitle = {CAV},
  year      = {2010},
  pages     = {24-40},
  editor    = {Tayssir Touili and Byron Cook and Paul Jackson},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6174},
}

@inproceedings{CCFHTTWZ:10:CLAAAGR,
  author    = {Yu-Fang Chen and Edmund M. Clarke and Azadeh Farzan and
               Fei He and Ming-Hsien Tsai and Yih-Kuen Tsay and
               Bow-Yaw Wang and Lei Zhu},
  title     = {Comparing Learning Algorithms in Automated Assume-Guarantee
               Reasoning},
  booktitle = {ISoLA (1)},
  year      = {2010},
  pages     = {643-657},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6415},
}

@inproceedings{CCFTTW:10:AAGRIL,
  author    = {Yu-Fang Chen and Edmund M. Clarke and Azadeh Farzan and
               Ming-Hsien Tsai and Yih-Kuen Tsay and Bow-Yaw Wang},
  title     = {Automated Assume-Guarantee Reasoning through Implicit Learning},
  booktitle = {CAV},
  year      = {2010},
  pages     = {511-526},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6174},
  editor    = {Tayssir Touili and Byron Cook and Paul Jackson},
}


@inproceedings{PRZ:01:ADVII,
  author    = {Amir Pnueli and Sitvanit Ruah and Lenore D. Zuck},
  title     = {Automatic Deductive Verification with Invisible Invariants},
  booktitle = {TACAS},
  year      = {2001},
  pages     = {82-97},
  editor    = {Tiziana Margaria and Wang Yi},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2031},
}

@inproceedings{N:07:SCAP,
  author    = {Kedar S. Namjoshi},
  title     = {Symmetry and Completeness in the Analysis of Parameterized
               Systems},
  booktitle = {VMCAI},
  year      = {2007},
  pages     = {299-313},
  editor    = {Byron Cook and Andreas Podelski},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4349},
}

@inproceedings{CN:07:LPGSP,
  author    = {Ariel Cohen and Kedar S. Namjoshi},
  title     = {Local Proofs for Global Safety Properties},
  booktitle = {CAV},
  year      = {2007},
  pages     = {55-67},
  editor    = {Werner Damm and Holger Hermanns},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4590},
}

@inproceedings{CN:08:LPLTPCP,
  author    = {Ariel Cohen and Kedar S. Namjoshi},
  title     = {Local Proofs for Linear-Time Properties of Concurrent Programs},
  booktitle = {CAV},
  year      = {2008},
  pages     = {149-161},
  editor    = {Aarti Gupta and Sharad Malik},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5123},
}

@article{CN:09:LPGSP,
  author    = {Ariel Cohen and Kedar S. Namjoshi},
  title     = {Local proofs for global safety properties},
  journal   = {Formal Methods in System Design},
  volume    = {34},
  number    = {2},
  year      = {2009},
  pages     = {104-125},
}


@inproceedings{CNY:10:DFCR,
  author    = {Ariel Cohen and Kedar S. Namjoshi and Yaniv Sa'ar},
  title     = {A Dash of Fairness for Compositional Reasoning},
  booktitle = {CAV},
  year      = {2010},
  editor    = {Tayssir Touili and Byron Cook and Paul Jackson},
  pages     = {543-557},
  volume    = {6174},
  publisher = {Springer},
  series    = {LNCS},
}

@Book{CLO:91:IVA,
  author =    {D. Cox and J. Little and D. O'Shea},
  title =        {Ideals, Varieties and Algorithms: An Introduction to
                  Computational Algebraic Geometry and Commutative Algebra},
  publisher =    {Springer},
  year =         {1991},
}

@InProceedings{SSM:04:NLIGGB,
  author =       {Siram Sankaranarayana and Henny B. Sipma and Zohar Manna},
  title =        {Non-linear Loop Invariant Generation using Gr{\"o}bner Bases},
  booktitle = {POPL},
  pages =     {318--329},
  year =      {2004},
  editor =    {Xavier Leroy},
  organization = {ACM},
}

@InProceedings{MS:04:PIALA,
  author =       {Markus M{\"u}ller-Olm and Helmut Seidl},
  title =        {Precise Interprocedural Analysis through Linear Algebra},
  booktitle = {POPL},
  pages =     {330--341},
  year =      {2004},
  editor =    {Xavier Leroy},
  organization = {ACM},
}

@Article{MS:04:CPPI,
  author =       {Markus M{\"u}ller-Olm and Helmut Seidl},
  title =        {Computing Polynomial Program Invariants},
  journal =      {Information Processing Letters},
  year =         {2004},
  volume =    {91},
  pages =     {233--244},
}

@Article{BBBKV:00:LFRMA,
  author =       {Amos Beimel and Francesco Bergadano and Nader H. Bshouty and
                  Stefano Varricchio},
  title =        {Learning Functions Represented as Multiplicity Automata},
  journal =      {JACM},
  year =         {2000},
  volume =    {47},
  number =    {5},
  pages =     {503--530},
  month =     {May},
}


@inproceedings{CCGR:99:NSMV,
  author =       {A. Cimatti and E.M. Clarke and F. Giunchiglia and M. Roveri},
  title =        {{\sc NuSMV}: a new {S}ymbolic {M}odel {V}erifier},
  booktitle =    {CAV},
  pages =        {495-499},
  year =         1999,
  editor =       {{N. H}albwachs and {D. P}eled},
  series =       {LNCS},
  number =       {1633},
  publisher =    {{S}pringer},
}

@Book{H:98:CM,
  author =    {Jim Handy},
  title =        {The Cache Memory Book},
  publisher =    {Academic Press},
  year =         {1998},
}

@inproceedings{SCCS:05:DCSA,
  author    = {Natasha Sharygina and Sagar Chaki and Edmund M. Clarke and
               Nishant Sinha},
  title     = {Dynamic Component Substitutability Analysis},
  booktitle = {FM},
  year      = {2005},
  pages     = {512-528},
  editor    = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3582},
}

@article{CAC:08:BUH,
  author    = {Jamieson M. Cobleigh and George S. Avrunin and
               Lori A. Clarke},
  title     = {Breaking Up is Hard to do: An Evaluation of Automated
                  Assume-Guarantee  Reasoning},
  journal   = {ACM Trans. Software Engineering Methodology},
  volume    = {17},
  number    = {2},
  year      = {2008},
}

@inproceedings{CS:07:OLAG,
  author    = {Sagar Chaki and Ofer Strichman},
  title     = {Optimized {$L^*$}-Based Assume-Guarantee Reasoning},
  booktitle = {TACAS},
  year      = {2007},
  pages     = {276-291},
  editor    = {Orna Grumberg and Michael Huth},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4424},
}

@article{CGJLV:03:CGAR,
  author    = {Edmund M. Clarke and Orna Grumberg and Somesh Jha and
               Yuan Lu and Helmut Veith},
  title     = {Counterexample-Guided Abstraction Refinement for Symbolic
               Model Checking},
  journal   = {J ACM},
  volume    = {50},
  number    = {5},
  year      = {2003},
  pages     = {752-794},
}

@article{B:95:ELBF,
  author    = {Nader H. Bshouty},
  title     = {Exact Learning {Boolean} Function via the Monotone Theory},
  journal   = {Information and Computation},
  volume    = {123},
  number    = {1},
  year      = {1995},
  pages     = {146-153},
}


@inproceedings{GMF:07:AAGC,
  author    = {Anubhav Gupta and Kenneth L. McMillan and Zhaohui Fu},
  title     = {Automated Assumption Generation for Compositional Verification},
  booktitle = {CAV},
  year      = {2007},
  pages     = {420-432},
  editor    = {Werner Damm and Holger Hermanns},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4590},
}


@article{GMF:08:AAGCV,
  author    = {Anubhav Gupta and Kenneth L. McMillan and Zhaohui Fu},
  title     = {Automated Assumption Generation for Compositional Verification},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {285-301},
}

@inproceedings{ACMN:05:SISJC,
  author    = {Rajeev Alur and Pavol Cern{\'y} and P. Madhusudan and
               Wonhong Nam},
  title     = {Synthesis of interface specifications for Java classes},
  booktitle = {POPL},
  year      = {2005},
  pages     = {98-109},
  editor    = {Jens Palsberg and Mart\'{\i}n Abadi},
  publisher = {ACM},
}



@inproceedings{AMN:05:SCVL,
  author    = {Rajeev Alur and P. Madhusudan and Wonhong Nam},
  title     = {Symbolic Compositional Verification by Learning Assumptions},
  booktitle = {CAV},
  year      = {2005},
  pages     = {548-562},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3576},
  editor    = {Kousha Etessami and Sriram K. Rajamani},
}

@article{NMA:08:ASCV,
  author    = {Wonhong Nam and P. Madhusudan and Rajeev Alur},
  title     = {Automatic Symbolic Compositional Verification by Learning
               Assumptions},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {207-234},
}

@inproceedings{SC:07:SBCV,
  author    = {Nishant Sinha and Edmund M. Clarke},
  title     = {{SAT}-Based Compositional Verification Using Lazy Learning},
  booktitle = {CAV},
  year      = {2007},
  pages     = {39-54},
  editor    = {Werner Damm and Holger Hermanns},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4590},
}


@inproceedings{CCST:05:AAGRSC,
  author    = {Sagar Chaki and Edmund M. Clarke and Nishant Sinha and
               Prasanna Thati},
  title     = {Automated Assume-Guarantee Reasoning for Simulation Conformance},
  booktitle = {CAV},
  year      = {2005},
  pages     = {534-547},
  editor    = {Kousha Etessami and Sriram K. Rajamani},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3576},
}


@article{CES:09:MC,
  author    = {Edmund M. Clarke and E. Allen Emerson and Joseph Sifakis},
  title     = {Model Checking: Algorithmic Verification and Debugging},
  journal   = {CACM},
  volume    = {52},
  number    = {11},
  year      = {2009},
  pages     = {74-84},
}


@inproceedings{CFCTW:09:LMSD,
  author    = {Yu-Fang Chen and Azadeh Farzan and Edmund M. Clarke and
               Yih-Kuen Tsay and Bow-Yaw Wang},
  title     = {Learning Minimal Separating DFA's for Compositional
               Verification},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5505},
  booktitle = {TACAS},
  year      = {2009},
  pages     = {31-45},
  editor    = {Stefan Kowalewski and Anna Philippou},
}


@inproceedings{GGP:07:RIAC,
  author    = {Mihaela Gheorghiu and Dimitra Giannakopoulou and
               Corina S. P{\u a}s{\u a}reanu},
  title     = {Refining Interface Alphabets for Compositional Verification},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4424},
  year      = {2007},
  pages     = {292-307},
  editor    = {Orna Grumberg and Michael Huth},
}


@article{GP:08:SILT,
  author    = {Dimitra Giannakopoulou and Corina S. P{\u a}s{\u a}reanu},
  title     = {Special Issue on Learning Techniques for Compositional
               Reasoning},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {173-174},
}


@inproceedings{BPG:08:AAGRAR,
  author    = {Mihaela Gheorghiu Bobaru and Corina S. P{\u a}s{\u a}reanu and
                  Dimitra Giannakopoulou},
  title     = {Automated Assume-Guarantee Reasoning by Abstraction Refinement},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5123},
  year      = {2008},
  pages     = {135--148},
  editor    = {Aarti Gupta and Sharad Malik},
}


@Book{CLO:91:IVA,
  author =    {D. Cox and J. Little and D. O'Shea},
  title =        {Ideals, Varieties and Algorithms: An Introduction to
                  Computational Algebraic Geometry and Commutative Algebra},
  publisher =    {Springer},
  year =         {1991},
}

@InProceedings{SSM:04:NLIGGB,
  author =       {Siram Sankaranarayana and Henny B. Sipma and Zohar Manna},
  title =        {Non-linear Loop Invariant Generation using Gr{\"o}bner Bases},
  booktitle = {POPL},
  pages =     {318--329},
  year =      {2004},
  editor =    {Xavier Leroy},
  organization = {ACM},
}

@InProceedings{MS:04:PIALA,
  author =       {Markus M{\"u}ller-Olm and Helmut Seidl},
  title =        {Precise Interprocedural Analysis through Linear Algebra},
  booktitle = {POPL},
  pages =     {330--341},
  year =      {2004},
  editor =    {Xavier Leroy},
  organization = {ACM},
}

@Article{MS:04:CPPI,
  author =       {Markus M{\"u}ller-Olm and Helmut Seidl},
  title =        {Computing Polynomial Program Invariants},
  journal =      {Information Processing Letters},
  year =         {2004},
  volume =    {91},
  pages =     {233--244},
}

@Book{H:98:CM,
  author =    {Jim Handy},
  title =        {The Cache Memory Book},
  publisher =    {Academic Press},
  year =         {1998},
}

@inproceedings{SCCS:05:DCSA,
  author    = {Natasha Sharygina and Sagar Chaki and Edmund M. Clarke and
               Nishant Sinha},
  title     = {Dynamic Component Substitutability Analysis},
  booktitle = {FM},
  year      = {2005},
  pages     = {512-528},
  editor    = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3582},
}

@inproceedings{GMF:07:AAGC,
  author    = {Anubhav Gupta and Kenneth L. McMillan and Zhaohui Fu},
  title     = {Automated Assumption Generation for Compositional Verification},
  booktitle = {CAV},
  year      = {2007},
  pages     = {420-432},
  editor    = {Werner Damm and Holger Hermanns},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4590},
}


@article{GMF:08:AAGCV,
  author    = {Anubhav Gupta and Kenneth L. McMillan and Zhaohui Fu},
  title     = {Automated Assumption Generation for Compositional Verification},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {285-301},
}


@inproceedings{AMN:05:SCVL,
  author    = {Rajeev Alur and P. Madhusudan and Wonhong Nam},
  title     = {Symbolic Compositional Verification by Learning Assumptions},
  booktitle = {CAV},
  year      = {2005},
  pages     = {548-562},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3576},
  editor    = {Kousha Etessami and Sriram K. Rajamani},
}

@inproceedings{CCST:05:AAGRSC,
  author    = {Sagar Chaki and Edmund M. Clarke and Nishant Sinha and
               Prasanna Thati},
  title     = {Automated Assume-Guarantee Reasoning for Simulation Conformance},
  booktitle = {CAV},
  year      = {2005},
  pages     = {534-547},
  editor    = {Kousha Etessami and Sriram K. Rajamani},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3576},
}


@article{CES:09:MC,
  author    = {Edmund M. Clarke and E. Allen Emerson and Joseph Sifakis},
  title     = {Model Checking: Algorithmic Verification and Debugging},
  journal   = {CACM},
  volume    = {52},
  number    = {11},
  year      = {2009},
  pages     = {74-84},
}


@inproceedings{CFCTW:09:LMSD,
  author    = {Yu-Fang Chen and Azadeh Farzan and Edmund M. Clarke and
               Yih-Kuen Tsay and Bow-Yaw Wang},
  title     = {Learning Minimal Separating DFA's for Compositional
               Verification},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5505},
  booktitle = {TACAS},
  year      = {2009},
  pages     = {31-45},
  editor    = {Stefan Kowalewski and Anna Philippou},
}


@inproceedings{GGP:07:RIAC,
  author    = {Mihaela Gheorghiu and Dimitra Giannakopoulou and
               Corina S. P{\u a}s{\u a}reanu},
  title     = {Refining Interface Alphabets for Compositional Verification},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4424},
  year      = {2007},
  pages     = {292-307},
  editor    = {Orna Grumberg and Michael Huth},
}


@article{GP:08:SILT,
  author    = {Dimitra Giannakopoulou and Corina S. P{\u a}s{\u a}reanu},
  title     = {Special Issue on Learning Techniques for Compositional
               Reasoning},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {173-174},
}


@inproceedings{BPG:08:AAGRAR,
  author    = {Mihaela Gheorghiu Bobaru and Corina S. P{\u a}s{\u a}reanu and
                  Dimitra Giannakopoulou},
  title     = {Automated Assume-Guarantee Reasoning by Abstraction Refinement},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5123},
  year      = {2008},
  pages     = {135--148},
  editor    = {Aarti Gupta and Sharad Malik},
}


@Article{W:93:ATRLF,
  author =       "Thomas Wilke",
  title =        "An Algebraic Theory for Regular Languages of Finite
                  and Infinite Words",
  journal =      "International Journal of Algebra and Computation",
  year =         "1993",
  volume =       "3",
  number =       "4",
  pages =        "447--489",
}

@INPROCEEDINGS{SAA:97:CFIV,
    author = "Jian Shen and Jacob Abraham and Adnan Aziz",
    title = "On Combining Formal and Informal Verification",
    booktitle = "CAV",
    year = "1997",
    pages = "376--387",
    editor = "O. Grumberg",
    volume = "1254",
    series = "LNCS",
    publisher = {Springer},
}

@Article{BZ:2008:AASPP,
  author =       "Marc Boul{\'e} and Zeljko ZilicK",
  title =        "Automata-based Assertion-checker Synthesis of {PSL}
                  Properties",
  journal =      "ACM Transactions on Design Automation of Electronic Systems",
  year =         "2008",
  volume =       "13",
  number =       "1",
}

@InProceedings{EFH:2003:RTLTP,
  author =       "C. Eisner and D. Fisman and J. Havlicek and
                  Y. Lustig and A. McIsaac and D. Van Campenhout",
  title =        "Reasoning with Temporal Logic on Truncated Paths",
  booktitle =    "CAV",
  pages =        "27 -- 39",
  year =         "2003",
  editor =       "W. A. Hunt Jr. and F. Somenzi",
  volume =       "2725",
  series =       "LNCS",
  publisher =    {Springer},
}

@Book{GTW:2002:ALIG,
  editor =    "E. Gr{\"a}del and W. Thomas and Th. Wilke",
  title =        "Automata, Logics, and Infinite Games",
  publisher =    "Springer",
  year =         "2002",
  volume =       "2500",
  series =       "LNCS",
}

@Article{BN:80:AL,
  author =       "L. Boasson and M. Nivat",
  title =        "Adherences of Languages",
  journal =      "Journal Computer and System Sciences",
  year =         "1980",
  volume =       "20",
  number =    "3",
  pages =        "285--309",
}

@Book{T:1991:TTFP,
  author =    "Simon Thompson",
  title =        "Type Theory and Functional Programming",
  publisher =    "Addison-Wesley",
  year =         "1991",
}

@Article{NM:1990:HHC,
  author =       "Gopalan Nadathur and Dale Miller",
  title =        "Higher-order Horn Clauses",
  journal =      "Journal of the ACM",
  year =         "1990",
  volume =       "37",
  number =       "4",
  pages =        "777--814",
}

@InProceedings{TW:2008:ACRICRP,
  author =       "Yih-Kuen Tsay and Bow-Yaw Wang",
  title =        "Automated Compositional Reasoning of Intuitionistically
                  Closed Regular Properties",
  booktitle =    "13th International Conference on Implementation and
                  Application of Automata",
  pages =        "36--45",
  year =         "2008",
  editor =       "Oscar H. Ibarra and Bala Ravikumar",
  volume =       "5148",
  series =       "LNCS",
  publisher =    {Springer},
}

@Manual{PSL:2007,
  title =        "Standard for Property Specification Language {(PSL)}",
  organization = "{IEEE}",
  year =         "2007",
  series =       "IEC",
  number =       "62531:2007 {(E)}"
}

@InProceedings{FCC:2008:EACV,
  author =       "Azadeh Farzan and Yu-Fang Chen and Edmund
                  M. Clarke and Yih-Kuen Tsay and Bow-Yaw Wang",
  title =        "Extending Automated Compositional Verification to
                  the Full Class of Omega-Regular Languages",
  booktitle =    "TACAS",
  pages =        "2--17",
  year =         "2008",
  editor =       "C.R. Ramakrishnan and J. Rehof",
  volume =       "4963",
  series =      "LNCS",
  publisher =    {Springer},
}


@Book{SU:2006:LCHI,
  author =    "Morten Heine S{\o}rensen and Pawel Urzyczyn",
  title =        "Lectures on Curry-Howard Isomorphism",
  publisher =    "Elsevier",
  year =         "2006",
  number =       "149",
  series =    "Studies in Logic and the Foundations of Mathematics",
}

@Article{B:1913:IF,
  author =       "L. E. J. Brouwer",
  title =        "Intuitionism and Formalism",
  journal =      "Bulletin of American Mathematical Society",
  year =         "1913",
  volume =    "20",
  pages =     "81--96",
}

@Book{H:1956:II,
  author =    "A. Heyting",
  title =        "Intuitionism: An Introduction",
  publisher =    "North-Holland Publishing",
  year =         "1971",
  edition =      "Third Revised",
}

@Book{J:2003:HLL,
  editor =    "Simon Peyton Jones",
  title =        "Haskell 98 Languages and Libraries: the Revised Report",
  publisher =    "Cambridge University Press",
  year =         "2003",
}

@Book{GJGB:2005:JLS,
  author =    "James Gosling and Bill Joy and Guy Steele and Gilad Bracha",
  title =        "{Java$^{\mbox{tm}}$} Language Specification",
  publisher =    "Prentice Hall",
  year =         "2005",
  edition =      "third",
}

@Article{PO:99:NAER,
  author =       "Jorge M. Pena and Arlindo L. Oliveira",
  title =        "A New Algorithm for Exact Reduction of Incompletely
                  Specified Finite State Machines",
  journal =      "IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systes",
  year =         "1999",
  volume =       "18",
  number =       "11",
  pages =        "1619--1632",
}

@Article{AFP:1992:LCHC,
  author =       "Dana Angluin and Michael Frazier and Leonard Pitt",
  title =        "Learning Conjunctions of Horn Clauses",
  journal =      "Machine Learning",
  year =         "1992",
  volume =       "9",
  pages =        "147--164",
  publisher =    "Kluwer Academic Publishers",
}

@InProceedings{AACW:2006:LCIV,
  author =       "Dana Angluin and James Aspnes and Jiang Chen and
                  Yinghua Wu",
  title =        "Learning a Circuit by Injecting Values",
  booktitle =    "Proceedings of the 38th ACM Symposium on Theory of
                  Computing",
  pages =        "584--593",
  year =         "2006",
  editor =       "Jon Kleinberg",
  publisher =    "ACM Press",
}

@InProceedings{CNP:1993:UPWRL,
  author =       "Hugues Calbrix and Maurice Nivat and Andreas Podelski",
  title =        "Ultimately Periodic Words of Rational $\omega$-Languages",
  booktitle =    "International Conference on Mathematical Foundations
                  of Programming Semantics",
  pages =        "554--566",
  year =         "1993",
  editor =       "Stephen D. Brookes and Michael G. Main and Austin Melton
                  and Michael W. Mislove and David A. Schmidt",
  volume =       "802",
  series =       "LNCS",
  publisher =    "Springer",
}

@Article{S:1990:SRC,
  author =       "Bertrand Le Sac",
  title =        "Saturating Right Congruences",
  journal =      "Informatique Th\'eoritique et Applications",
  year =         "1990",
  volume =       "24",
  number =       "6",
  pages =        "545--560",
}

@Article{MP:1995:OLIRS,
  author =       "Oded Maler and Amir Pnueli",
  title =        "On the Learnability of Infinitary Regular Sets",
  journal =      "Information and Computation",
  year =         "1995",
  volume =       "118",
  number =    "2",
  pages =     "316--326",
}

@Article{RS:1993:IFAUHS,
  author =       "Ronald L. Rivest and Robert E. Schapire",
  title =        "Inference of Finite Automata Using Homing Sequences",
  journal =      "Information and Computation",
  year =         "1993",
  volume =       "103",
  number =       "2",
  pages =        "299-347",
}

@InProceedings{W:2007:ADCR,
  author =       "Bow-Yaw Wang",
  title =        "Automatic Derivation of Compositional Rules in
                  Automated Compositional Reasoning",
  booktitle =    "CONCUR",
  pages =        "303--316",
  year =         "2007",
  editor =       "Luis Caires and Vasco T. Vasconcelos",
  volume =       "4703",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{HW:2007:CSBMC,
  author =       "Geng-Dian Huang and Bow-Yaw Wang",
  title =        "Complete {SAT}-based Model Checking for Context-Free
                  Processes",
  booktitle =    "Automated Technology for Verification and Analysis",
  year =         "2007",
  editor =       "Kedar Namjoshi and Tomohiro Yoneda",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{W:2006:SMAE,
  author =       "Bow-Yaw Wang",
  title =        "On the Satisfiability of Modular Arithmetic Formulae",
  booktitle =    "Automated Technology for Verification and Analysis",
  pages =        "186--199",
  year =         "2006",
  editor =       "Susanne Graf and Wenhui Zhang",
  volume =       "4218",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{TW:2006:FCCIC,
  author =       "Ming-Hsien Tsai and Bow-Yaw Wang",
  title =        "Formalization of {CTL$^*$} in the Calculus of Inductive
                  Constructions",
  booktitle =    "Asian Computing Science Conference",
  year =         "2006",
  address =      "Tokyo, Japan",
  month =        "December",
}

@InProceedings{TW:2006:MFRMC,
  author =       "Ming-Hsien Tsai and Bow-Yaw Wang",
  title =        "Modular Formalization of Reactive Modules in {Coq}",
  booktitle =    "Asian Computing Science Conference",
  year =         "2006",
  address =      "Tokyo, Japan",
  month =        "December",
}

@InProceedings{ES:2003:ESAT,
  title =	"An Extensible {SAT}-solver",
  author =	"Niklas E{\'e}n and Niklas S{\"o}rensson",
  publisher =	"Springer",
  year = 	"2003",
  volume =	"2919",
  booktitle =	"SAT",
  editor =	"Enrico Giunchiglia and Armando Tacchella",
  pages =	"502--518",
  series =	"LNCS",
}

@INPROCEEDINGS{M:2004:ILTL,
  AUTHOR    = "Patrick Maier",
  EDITOR    = "Jerzy Marcinkowski and Andrzej Tarlecki",
  TITLE     = "Intuitionistic {LTL} and a New Characterization of
                  Safety and Liveness",
  BOOKTITLE = "Computer Science Logic",
  PUBLISHER = "Springer",
  SERIES    = "LNCS",
  VOLUME    = "3210",
  YEAR      = "2004",
  PAGES     = "295--309",
}

@INPROCEEDINGS{M:2003:CCAG,
  AUTHOR    = "Patrick Maier",
  EDITOR    = "Andrew D. Gordon",
  TITLE     = "Compositional Circular Assume-Guarantee Rules Cannot Be
                  Sound and Complete",
  BOOKTITLE = "Foundations of Software Science and Computational Structures",
  PUBLISHER = "Springer",
  SERIES    = "LNCS",
  VOLUME    = "2620",
  YEAR      = "2003",
  PAGES     = "343--357",
}


@Article{AS:1987:RSL,
  author =       "Bowen Alpern and Fred B. Schneider",
  title =        "Recognizing Safety and Liveness",
  journal =      "Distributed Computing",
  year =         "1987",
  volume =       "2",
  number =       "3",
  pages =        "117--126",
}

@Book{FKL:2003:ABD,
  author =    "Harry D. Foster and Adam C. Krolnik and David J. Lacey",
  title =     "Assertion-Based Design",
  publisher = "Springer",
  year =      "2003",
}

@incollection{S:1997:OL,
  author =    "Ludwig Staiger",
  editor =    "G. Rozenberg and A. Salomaa",
  title =     "$\omega$-languages",
  chapter =      "6",
  publisher =    "Springer",
  year =         "1997",
  volume =    "3",
  booktitle =    "Handbook of Formal Languages",
  pages =     "339-387",
}

@incollection{BE:2001:MIR,
  author = "Olaf Burkart and Javier Esparza",
  title = "More Infinite Results",
  booktitle = "Current Trends in Theoretical Computer Science,
               Entering the 21th Century",
  pages = "480--503",
  editor = "Gheorghe Paun and Grzegorz Rozenberg and Arto Salomaa",
  publisher = "World Scientific",
  year = "2001",
}

@InProceedings{D:1998:DAMCAI,
  author =       "David A. Schmidt",
  title =        "Data Flow Analysis is Model Checking of Abstract
                  Interpretation",
  booktitle =    "POPL",
  pages =        "38--48",
  year =         "1998",
  OPTeditor =    {},
  publisher =    "ACM Press",
}

@Article{W:2001:PPGMC,
  author =       "Igor Walukiewicz",
  title =        "Pushdown Processes: Games and Model-Checking",
  journal =      "Information and Computation",
  year =         "2001",
  volume =       "164",
  number =       "2",
  pages =        "234--263",
  publisher =    "Academic Press",
}

@InProceedings{CM:1991:TGAG,
  author =       "Didier Caucal and Roland Monfort",
  title =        "On the Transition Graphs of Automata and Grammars",
  booktitle =    "Graph-Theoretic Concepts in Computer Science",
  pages =        "311--337",
  year =         "1990",
  editor =       "Rolf H. M{\"o}hring",
  volume =       "484",
  series =       "LNCS",
  publisher =    "Springer",
}

@Article{MS:1985:TEPASL,
  author =       "David E. Muller and Paul E. Schupp",
  title =        "The Theory of Ends, Pushdown Automata, and
                  Sceond-Order Logic",
  journal =      "Theoretical Computer Science",
  year =         "1985",
  volume =       "37",
  OPTnumber =    {},
  pages =        "51--75",
  publisher =    "Elsevier Science Publishers",
}

@article{CH:1993:DIIP,
  author = "S. Christensen and H. H{\"u}ttel",
  title = "Decidability issues for infinite-state processes - a survey",
  journal = "Bulletin of the European Association for Theoretical
             Computer Science",
  volume = "51",
  pages = "156--166",
  year = "1993",
}

@InProceedings{AM:2004:VPL,
  author =       "R. Alur and P. Madhusudan",
  title =        "Visibly Pushdown Languages",
  booktitle =    "36th ACM Symposium on Theory of Computing",
  pages =        "202--211",
  year =         "2004",
  publisher =    "ACM Press",
}

@TechReport{W:2007:ADCRACR,
  author =       "Bow-Yaw Wang",
  title =        "Automatic Derivation of Compositional Rules in
                  Automated Compositional Reasoning",
  institution =  "Institute of Information Science, Academia Sinica",
  year =         "2007",
  number =       "TR-IIS-07-002"
}

@Article{HS:1994:LMCCFP,
  author =       "H. Hungar and B. Steffen",
  title =        "Local Model Checking for Context-Free Processes",
  journal =      "Nordic Journal of Computing",
  year =         "1994",
  volume =       "1",
  number =       "3",
  pages =        "364--385",
}

@Book{G:2006:TCAL,
  author =       "Robert Goldblatt",
  title =        "Topoi: The Categorial Analysis of Logic",
  publisher =    "Dover Publications",
  year =         "2006",
  edition =      "revised",
}

@Book{TS:2000:BPT,
  author =       "A. S. Troelstra and H. Schwichtenberg",
  title =        "Basic Proof Theory",
  publisher =    "Cambridge University Press",
  year =         "2000",
  number =       "43",
  series =       "Cambridge Tracts in Theoretical Computer Science",
}

@Book{RBHHLRZ:2001:CVICNM,
  author =    "Willem-Paul de Roever and Frank de Boer and Ulrich
                  Hanneman and Jozef Hooman and Yassine Lakhnech and
                  Mannes Poel and Job Zwiers",
  title =        "Concurrency Verification: Introduction to
                  Compositional and Noncompositional Methods",
  publisher =    "Cambridge University Press",
  year =         "2001",
  number =       "54",
  series =       "Cambridge Tracts in Theoretical Computer Science",
}

@InProceedings{BGP:2003:PRACVL,
  author =       "Howard Barringer and Dimitra Giannakopoulou and
                  Corina S. P{\u a}s{\u a}reanu",
  title =        "Proof Rules for Automated Compositional Verification
                  through Learning",
  booktitle =    "Workshop on Specification and Verification of
                  Component-Based Systems",
  pages =        "14--21",
  year =        "2003",
}

@InProceedings{CGP:2003:LACV,
  author =       "Jamieson M. Cobleigh and Dimitra Giannakopoulou and
                  Corina S. P{\u a}s{\u a}reanu",
  title =        "Learning Assumptions for Compositional Verification",
  booktitle =    "TACAS",
  pages =        "331--346",
  year =         "2003",
  editor =       "Hubert Garavel and John Hatcliff",
  volume =       "2619",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{YW:2004:TUMCRA,
  author =       "Fang Yu and Bow-Yaw Wang",
  title =        "Toward Unbounded Model Checking for Region
                  Automata",
  booktitle =    "Automated Technology for Verification and Analysis",
  pages =        "20--33",
  year =         "2004",
  editor =       "Farn Wang",
  volume =       "3299",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{YWH:2004:BMCRA,
  author =       "Fang Yu and Bow-Yaw Wang and Yao-Wen Huang",
  title =        "Bounded Model Checking for Region Automata",
  booktitle =    "Joint International Conferences on Formal Modelling
                  and Analysis of Timed Systems (FORMATS)
                  and Formal Techniques in Real-Time and
                  Fault-Tolerant Systems (FTRTFT)",
  pages =        "246--262",
  year =         "2004",
  editor =       "Yassine Lakhnech and Sergio Yovine",
  volume =       "3253",
  series =       "LNCS",
  publisher =    "Springer",
}

@Article{W:2004:EVTABDS,
  author =       "Farn Wang",
  title =        "Efficient Verification of Timed Automata with {BDD}-like
                  Data-Structures",
  journal =      "Journal of Software Tools for Technology Transfer (STTT)",
  year =         "2004",
  volume =       "6",
  number =       "1",
  month =        "July",
  pages =        "77--97",
  publisher =    "Springer",
}

@InProceedings{BLLPY:1995:UTSAVRTS,
  title =    "{\sc Uppaal} --- a Tool Suite for Automatic Verification of
                  Real--Time Systems",
  author =   "Johan Bengtsson and Kim G. Larsen and Fredrik Larsson
                  and Paul Pettersson and Wang Yi",
  booktitle = "Workshop on Verification and Control of Hybrid Systems
                  III",
  series = "LNCS",
  volume = "1066",
  pages = "232--243",
  publisher = "Springer",
  year = "1995",
}

@Article{Y:1997:KVTRTS,
  author =       "S. Yovine",
  title =        "Kronos: A Verification Tool for Real-Time Systems",
  journal =      "International Journal of Software Tools for
                  Technology Transfer",
  year =         "1997",
  volume =       "1",
  number =       "1--2",
  pages =        "123--133",
  month =        "October",
  publisher =    "Springer",
}

@InProceedings{SB:2003:UFSMC,
  author    = "Sanjit A. Seshia and Randal E. Bryant",
  title     = "Unbounded, Fully Symbolic Model Checking of Timed
                  Automata using Boolean Methods",
  booktitle = "CAV",
  editor    = "Warren A. Hunt Jr. and Fabio Somenzi",
  volume    = "2725",
  series    = "LNCS",
  year      = "2003",
  pages     = "154--166",
  publisher = "Springer",
}


@InProceedings{PWZ:2002:TBMCUFT,
  author =    "Wojciech Penczek and Bozena Wozna and Andrzej Zbrzezny",
  title =     "Towards Bounded Model Checking for the Universal
                  Fragment of TCTL",
  booktitle = "Formal Techniques in Real-Time and Fault
                  Tolerant Systems ({FTRTFT}'02)",
  volume =    "2469",
  series =    "LNCS",
  pages =     "265--288",
  publisher = "Springer",
  year =      "2002",
}

@InProceedings{MORRSST:2004:SAL,
  author =    "Leonardo de Moura and Sam Owre and Harald Rue{\ss} and
               John Rushby and N. Shankar and Maria Sorea and
               Ashish Tiwari",
  title =     "{SAL} 2",
  booktitle = "CAV",
  year =      "2004",
  series =    "LNCS",
  address =   "Boston",
  month =     "July",
  publisher = "Springer",
}

@InProceedings{MRS:2002:PADRTS,
  author =       "M. Oliver M{\"o}ller and Harald Ru{\ss} and Maria Sorea",
  title =        "Predicate Abstraction for Dense Real-Time Systems",
  booktitle =    "Theory and Practice of Timed Systems ({TPTS}'2002)",
  series =       "Electronic Notes in Theoretical Computer Science",
  year =         "2002",
  volume =       "65",
  number =       "2",
}

@InProceedings{AKMM:2003:EADTBMC,
  author =       "Nina Amla and Robert Kurshan and Kenneth L. McMillan
                  and Ricardo Medel",
  title =        "Experimental Analysis of Different Techniques for
                  Bounded Model Checking",
  booktitle =    "TACAS",
  pages =        "34--48",
  year =         "2003",
  editor =       "H. Garavel and J. Hatcliff",
  volume =       "2619",
  series =       "LNCS",
  publisher =    "Springer",
}

@Article{R:2001:AFCTL,
  author =       "Mark Reynolds",
  title =        "An Axiomatization of Full Computation Tree Logic",
  journal =      "Journal of Symbolic Logic",
  year =         "2001",
  volume =       "66",
  number =       "3",
  pages =        "1011--1057",
  month =        "September",
}

@Article{ZPS:2005:FMPSUC,
  author =       "Xinwen Zhang and Francesco Parisi-Presicce and Ravi
                  Sandhu",
  title =        "Formal Model and Policy Specification of Usage Control",
  journal =      "ACM Transactions on Information and System Security",
  year =         "2005",
  volume =       "8",
  number =       "4",
  pages =        "351--387",
  month =        "November",
}

@Book{K:1987:TLP,
  author =       "Fred Kr{\"o}ger",
  title =        "Temporal Logic of Programs",
  publisher =    "Springer",
  year =         "1987",
}

@Book{YC:2004:ITPPDC,
  author =       "Yves Bertot and Pierre Cast\'eran",
  title =        "Interactive Theorem Proving and Program
                  Development -- Coq'Art: The Calculus of Inductive
                  Constructions",
  publisher =    "Springer",
  year =         "2004",
  series =       "Texts in Theoretical Computer Science",
}

@InProceedings{MN:1995:CMCDIOA,
  author =       "O. M{\"u}ller and T. Nipkow",
  title =        "Combining Model Checking and Deduction for {I/O}-Automata",
  booktitle =    "Proc. of {TACAS}",
  pages =        "1--16",
  year =         "1995",
  editor =       "Ed Brinksma and Rance Cleaveland and Kim Guldstrand
                  Larsen and Tiziana Margaria and Bernhard Steffen",
  volume =       "1019",
  series =       "LNCS",
  publisher =    "Springer",
}

@Book{GBDJMS:1994:PVM,
  author =    "Al Geist and Adam Beguelin and Jack Dongarra and
                  Weicheng Jiang and Robert Manchek and Vaidy Sunderam",
  title =        "PVM: Parallel Virtual Machine -- A Users' Guide and
                  Tutorial for Networked Parallel Computing",
  publisher =    "The MIT Press",
  year =         "1994",
}

@InProceedings{ST:2002:PIM,
  author =       "M. Stehr and C. Talcott",
  title =        "Plan in Maude: Specifying an active network
                  programming language",
  booktitle =    "Workshop on Rewriting Logic and Its Applications",
  year =         "2002",
  volume =       "71",
  series =       "Electronic Notes in Theoretical Computer Science",
  publisher =    "Elsevier",
}

@InProceedings{RRSDDRV:2000:XMC,
  author =       "C. R. Ramakrishnan and I. V. Ramakrishnan and Scott
                  A. Smolka and Yifei Dong and Xiaoqun Du and Abhik
                  Roychoudhury and V. N. Venkatakrishnan",
  title =        "XMC: A Logic-Programming-Based Verification Toolset",
  booktitle =    "CAV",
  editor=        "E. Allen Emerson and A. Prasad Sistla",
  pages =        "576--580",
  year =         "2000",
  volume =       "1855",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{W:2006:MAADSLRR,
  author =       "Bow-Yaw Wang",
  title =        "Modeling and Analyzing Applications with
                  Domain-Specific Languages by Reflective Rewriting: a
                  Case Study",
  booktitle =    "21st ACM Symposium on Applied Computing",
  pages =        "1773--1778",
  year =         "2006",
  publisher =    "ACM"
}

@InProceedings{W:2006:AVMCR,
  author =       "Bow-Yaw Wang",
  title =        "Automatic Verification of a Model Checker by Reflection",
  booktitle =    "8th International Symposium, PADL",
  pages =        "45--59",
  year =         "2006",
  editor =       "Pascal Van Hentenryck",
  volume =       "3819",
  series =       "LNCS",
  address =      "Charleston, USA",
  month =        "January",
  publisher =    "Springer",
}

@Book{M:1981:ALPCP,
  author =    "B. A. Murtagh",
  title =     "Advanced Linear Programming: Computation and Practice",
  publisher =    "McGrawHill",
  year =         "1981",
}

@Article{H:1969:ABCP,
  author =       "C. A. R. Hoare",
  title =        "An axiomatic basis for computer programming",
  journal =      "Communications of the ACM",
  year =         "1969",
  volume =       "12",
  number =       "10",
  pages =        "576--585",
}

@Manual{B:2001:SPC,
  title =        "Some properties of {CTL}",
  author =       "Gertrud Bauer",
  organization = "Technische Universit{\"a}t M{\"u}nchen",
  year =         "2001",
  note =         "{Isabelle/Isar} document",
}

@Manual{M:1998:ITLA,
  title =        "{I}sabelle/{TLA}",
  author =       "Stephan Merz",
  year =         "1998",
  organization = "Technische Universit{\"a}t M{\"u}nchen",
  note =         "{Isabelle/Isar} document",
}

@Article{SCG:2003:ALTLCOC,
  author =       "Solange Coupet-Grimal",
  title =        "An Axiomatization of Linear Temporal Logic in The Calculus of
                  Inductive Constructions",
  journal =      "Logic and Computation",
  year =         "2003",
  volume =       "13",
  number =       "6",
  pages =        "801--813",
}

@Article{M:2001:OFOMM,
  author =       "Marino Miculan",
  title =        "On the Formalization of the Modal $\mu$-Calculus in the
                  Calculus of Inductive Constructions",
  journal =      "Information and Computation",
  year =         "2001",
  volume =       "164",
  number =       "1",
  pages =        "199--231",
}

@InProceedings{DFH:1995:HOASC,
  author =       "Jo{\"e}lle Despeyroux and Amy P. Felty and Andr{\'e}
                  Hirschowitz",
  title =        "Higher-Order Abstract Syntax in Coq",
  booktitle =    "Typed Lambda Calculi and Applications",
  pages =        "124--138",
  year =         "1995",
  editor =       "Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin",
  volume =       "902",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{MN:1997:TOIOAb,
  author =       "Olaf M{\"u}ller and Tobias Nipkow",
  title =        "Traces of {I/O} Automata in {Isabelle}/{HOLCF}",
  booktitle =    "Theory and Practice of Software Development",
  pages =        "580--595",
  year =         "1997",
  editor =       "M. Bidoit and M. Dauchet",
  volume =       "1214",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{M:1998:IOAAB,
  author =       "Olaf M{\"u}ller",
  title =        "{I/O} Automata and Beyond - Temporal Logic and
                  Abstraction in {Isabelle}",
  booktitle =    "Theorem Proving in Higher Order Logics",
  pages =        "331--348",
  year =         "1998",
  editor =       "J. Grundy and M. Newey",
  volume =       "1479",
  series =       "LNCS",
  publisher =    "Springer",
}

@PhdThesis{M:1998:VEFIOA,
  author =       "Olaf M{\"u}ller",
  title =        "A Verification Environment for {I/O} Automata Based on
                  Formalized Meta-Theory",
  school =       "Technische Universit{\"a}t M{\"u}nchen",
  year =         "1998",
}

@InProceedings{NS:1995:IOII,
  author =       "Tobias Nipkow and Konrad Slind",
  title =        "{I/O} Automata in {Isabelle}/{HOL}",
  booktitle =    "Types for Proofs and Programs",
  pages =        "101--119",
  year =         "1995",
  editor =    "P. Dybjer and B. Nordstr{\"o}m and J. Smith",
  volume =    "996",
  series =    "LNCS",
  publisher = "Springer",
}

@InProceedings{BB:2004:CVCL,
  author    = "Clark Barrett and Sergey Berezin",
  title     = "{CVC L}ite: A New Implementation of the Cooperating
                  Validity Checker",
  booktitle = "CAV",
  series    = "LNCS",
  volume    = "3114",
  publisher = "Springer",
  editor    = "Rajeev Alur and Doron A. Peled",
  pages     = "515--518",
  year      = "2004",
}

@TechReport{W:2006:OTSOMA,
  author =       "Bow-Yaw Wang",
  title =        "On the Satisfiability of Modular Arithmetic Formula",
  institution =  "Institute of Information Science, Academia Sinica",
  year =         "2006",
  number =    "TR-IIS-06-001",
  month =     "January",
  note =      "http://www.iis.sinica.edu.tw/LIB/TechReport/tr2006/tr06.html",
}

@Book{S:1995:CTAP,
  author =    "Douglas R. Stinson",
  title =        "Cryptography: Theory and Practice",
  publisher =    "CRC Press, Inc",
  year =         "1995",
}

@InProceedings{BD:2002:RDVUILP,
  author =       "Raik Brinkmann and Rolf Drechsler",
  title =        "{RTL}-Datapath Verification using Integer Linear Programming",
  booktitle =    "ASP-DAC/VLSI Design",
  pages =     "741",
  year =      "2002",
  publisher = "IEEE Computer Society",
}

@InProceedings{BW:2002:RACWFA,
  author =       "Bernard Boigelot and Pierre Wolper",
  title =        "Representing Arithmetic Constraints with Finite
                  Automata: An Overview",
  booktitle =    "International Conference on Logic Programming",
  pages =     "1--19",
  year =      "2002",
  editor =    "Peter J. Stuckey",
  volume =    "2401",
  series =    "LNCS",
  publisher = "Springer",
}

@InProceedings{SB:2004:DQFPFUP,
  author =       "Sanjit A. Seshia and Randal E. Bryant",
  title =        "Deciding Quantifier-Free Presburger Formulas Using
                  Parameterized Solution Bounds",
  booktitle =    "Logic in Computer Science",
  pages =     "100--109",
  year =      "2004",
  publisher = "IEEE Computer Society",
}

@InProceedings{W:2005:PFMCPWS,
  author =       "Bow-Yaw Wang",
  title =        "Proving $\forall\mu$-Calculus Properties with {SAT}-Based
                  Model Checking",
  booktitle =    "FORTE",
  pages =        "113--127",
  year =         "2005",
  editor =       "Farn Wang",
  volume =       "3731",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{CCGJV:2003:MVOSCC,
  author =       "Sagar Chaki and Edmund Clarke and Alex Groce and
                  Somesh Jha and Helmut Veith",
  title =        "Modular Verification of Software Components in {C}",
  booktitle =    "International Conference on Software Engineering",
  pages =        "385--395",
  year =         "2003",
  editor =    "Laurie Dillon and Walter Tichy",
  publisher = "IEEE Computer Society",
}

@Article{CKSY:2004:PAOAC,
  author =       "Edmund Clarke and Daniel Kroening and Natasha
                  Sharygina and Karen Yorav",
  title =        "Predicate Abstraction of {ANSI-C} Programs Using {SAT}",
  journal =      "Formal Methods in System Design",
  year =         "2004",
  volume =       "25",
  number =       "2--3",
  pages =        "105--127"
}

@InProceedings{P:1991:TOT,
  author =       "William Pugh",
  title =        "The Omega test: a fast and practical integer
                  programming algorithm for dependence analysis",
  booktitle =    "1991 {ACM}/{IEEE} conference on Supercomputing",
  editor =    "Joanne L. Martin",
  pages =     "4--13",
  year =      "1991",
  publisher = "ACM Press",
}

@InProceedings{G:1991:SSOLCEAV,
  author =       "Philippe Granger",
  title =        "Static analysis of linear congruence equalities
                  among variables of a program",
  booktitle =    "Theory and Practice of Software Ddevelopment",
  pages =        "169--192",
  year =        "1991",
  editor =       "Samson Abramsky and T. S. E. Maibaum",
  volume =       "439",
  series =       "LNCS",
  publisher =    "Springer",
}

@TechReport{BM:2005:MADP,
  author =       "Domagoj Babi\'c and Madanlal Musuvathi",
  title =        "Modular Arithmetic Decision Procedure",
  institution =  "Microsoft Research",
  year =         "2005",
  number =       "MSR-TR-2005-114",
}

@InProceedings{MS:2005:AGFFIAONP,
  author =       "Markus M{\"u}ller-Olm and Helmut Seidl",
  title =        "A Generic Framework for Interprocedural Analysis of
                  Numerical Properties",
  booktitle =    "Satatic Analysis",
  pages =        "235--250",
  year =         "2005",
  editor =       "Chris Hankin and Igor Siveroni",
  volume =       "3672",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{MS:2005:AOMA,
  author =       "Markus M{\"u}ller-Olm and Helmut Seidl",
  title =        "Analysis of Modular Arithmetic",
  booktitle =    "Programming Languages and Systems",
  pages =        "31--45",
  year =      "2005",
  editor =    "Mooly Sagiv",
  volume =    "3444",
  series =    "LNCS",
  publisher = "Springer",
}

@Book{D:1993:LPAE,
  author =    "George B. Dantzig",
  title =        "Linear Programming and Extensions",
  publisher =    "Princeton University Press",
  year =         "1993",
  edition =   "10",
}

@Book{K:1997:TAOC,
  author =    "Donald E. Knuth",
  title =        "The Art of Computer Programming",
  publisher =    "Addison-Wesley",
  year =         "1997",
  volume =    "II, Seminumerical Algorithms",
}

@InProceedings{RL:1978:PAWBQA,
  author =       "C. R. Reddy and D. W. Loveland",
  title =        "Presburger Arithmetic with Bounded Quantifier Alternation",
  year =         "1978",
  booktitle =    "ACM Symposium on Theory of Computing",
  pages =        "320--325",
  organization = "ACM",
}

@InProceedings{O:1973:EBFPA,
  author =       "Derek C. Oppen",
  title =        "Elementary Bounds for Presburger Arithmetic",
  year =         "1973",
  booktitle =    "ACM Symposium on Theory of Computing",
  pages =        "34--37",
  organization = "ACM",
}

@Article{C:1972:TPIAWM,
  author =       "D. C. Cooper",
  title =        "Theorem Proving in Arithmetic without Multiplication",
  journal =      "Machine Intelligence",
  year =         "1972",
  volume =       "7",
}

@InProceedings{RG:2005:TSCLFMIP,
  author =       "T. K. Ralphs and M. Guzelsoy",
  title =        "The {SYMPHONY} Callable Library for Mixed Integer
                  Programming",
  year =         "2005",
  booktitle =    "INFORMS Computing Society",
}


@Manual{SCHEME,
  author =       "IEEE",
  title =        "IEEE Standard for the Scheme Programming Language",
  publisher =    "IEEE",
  year =         "1991",
  number =       "1178-1990",
  series =       "IEEE Standard",
}

@Book{P:1994:CC,
  author =    "Christos H. Papadimitriou",
  title =        "Computational Complexity",
  publisher =    "Addison-Wesley",
  year =         "1994",
}

@Book{PS:1982:COAAC,
  author =    "Christos H. Papadimitriou and Kenneth Steiglitz",
  title =        "Combinatorial Optimization: Algorithms and Complexity",
  publisher =    "Prentice-Hall, Inc",
  year =         "1982",
}

@Book{H:1980:A,
  author =    "Thomas W. Hungerford",
  title =        "Algebra",
  publisher =    "Springer",
  year =         "1980",
  volume =    "73",
  series =    "Graduate Texts in Mathematics",
}

@Book{GJ:1979:CAI,
  author =    "Michael R. Garey and David S. Johnson",
  title =        "Computers and Intractability: A Guide to the Theory
                  of NP-Completeness",
  publisher =    "W. H. Freeman and company",
  year =         "1979",
}

@Book{NZ:1980:AITTTON,
  author =    "Ivan Niven and Herbert S. Zuckerman",
  title =        "An Introduction to the Theory of Numbers",
  publisher =    "John Wiley \& Sons, Inc",
  year =         "1980",
  edition =      "fourth",
}

@InProceedings{SLAM,
  author =       "Thomas Ball and Sriram K. Rajamani",
  title =        "The {SLAM} Toolkit",
  booktitle =    "Computer Aided Verification",
  pages =        "260--264",
  year =         "2001",
  editor =       "G/'erard Berry and Hubert Comon and Alain Finkel",
  volume =       "2102",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{BLAST,
  author =       "Thomas A. Henzinger and Ranjit Jhala and Rupak
                  Majumdar and Gregoire Sutre",
  title =        "Software Verification with {Blast}",
  booktitle =    "10th SPIN Workshop on Model Checking Software",
  pages =        "235--239",
  year =         "2003",
  editor =       "Thomas Ball and Sriram K. Rajamani",
  volume =       "2648",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{VSVA:2005:ULITVORP,
  author =       "Abhay Vardhan and Koushik Sen and Mahesh Viswanathan
                  and Gul Agha",
  title =        "Using Language Inference to Verify Omega-Regular
                  Properties",
  booktitle =    "Tools and Algorithms for the Construction and
                  Analysis of Systems",
  pages =        "45--60",
  year =         "2005",
  editor =       "N. Halbwachs and L. Zuck",
  volume =       "3440",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{WC:2005:MTSFED,
  author =       "Westley Weimer and George C. Necula",
  title =        "Mining Temporal Specifications for Error Detection",
  booktitle =    "Tools and Algorithms for the Construction and
                  Analysis of Systems",
  pages =        "461--476",
  year =         "2005",
  editor =       "N. Halbwachs and L. Zuck",
  volume =       "3440",
  series =       "LNCS",
  publisher =    "Springer",
}

@Book{Burk97b,
  author =    "Rainer Burkhardt",
  title =        "{UML}-Unified Modeling Language",
  publisher =    "Addison Wesley",
  year =         "1997",
  ISBN =      "3-8273-1226-4",
}

@Book{IB-A935003,
  author =    "John R. Levine and Tony Mason and Doug Brown",
  title =     "Lex \& Yacc",
  publisher = "O'Reilly",
  year =      "1992",
  address =   "Sebastopol",
  edition =   "2",
}

@Manual{KERNIGNAN77A,
  title =     "The {M4} Macro Processor",
  author =    "B. W. Kernighan and D. M. Ritchie",
  organization = "Bell Laboratories",
  address =   "Murray Hill, NJ",
  month =     "July",
  year =      "1977",
}

@Book{SGG:2004:OSC,
  author =       "Avi Silberschatz and Peter Baer Galvin and Greg Gagne",
  title =        "Operating System Concepts",
  publisher =    "John Wiley \& Sons, Inc.",
  year =         "2004",
  edition =      "7th",
  ISBN =         "ISBN 0-471-69466-5",
}

@InProceedings{CMP:2004:FPSRSR,
  author =       "Manuel Clavel and Narciso Mart\'i-Oliet and Miguel Palomino",
  title =        "Formalizing and Proving Semantic Relations between Specifications by Reflection",
  booktitle =    "Algebraic Methodology and Software Technology: 10th International Conference",
  pages =        "72--86",
  year =         "2004",
  editor =       "Stirling",
  volume =       "3116",
  series =       "LNCS",
  OPTpublisher = "Springer",
}

@TechReport{Wang:2005:AVMCRL,
  author =       "Bow-Yaw Wang",
  title =        "Automatic Verification of a Model Checker in Rewriting Logic",
  institution =  "Institute of Information Science, Academia Sinica",
  year =         "2005",
  number =       "TR-IIS-05-009",
  note =          "http://www.iis.sinica.edu.tw/LIB/TechReport/tr2005/tr05009.pdf",
}


@Manual{Clavel:2004:ITP,
  author =       "Manuel Clavel",
  title =        "The {ITP} Tool - An Inductive Theorem Prover Tool for Maude Membership Equational Specifications",
  institution =  "Facultad de Informatica, Universidad Complutense de Madrid",
  year =         "2004",
  URL =          "http://maude.cs.uiuc.edu/maude1/tools/itp/",
}


@Article{ZantemaPol:2001:RABDD,
  author =       "Hans Zantema and Jaco van de Pol",
  title =        "A rewriting approach to binary decision diagrams",
  journal =      "Journal of Logic and Algebraic Programming",
  year =         "2001",
  volume =       "49",
  Tnumber =      "1--2",
  pages =        "61--86",
  publisher =    "Elsevier Science Publishers",
}


@InProceedings{PolZantema:2000:BDDSR,
  author =       "Jaco van de Pol and Hans Zantema",
  title =        "Binary Decision Diagrams by Shared Rewriting",
  year =         "2000",
  editor =       "Mogens Nielsen and Branislav Rovan",
  booktitle =    "Mathematical Foundations of Computer Science 2000, 25th International Symposium",
  pages =        "609--618",
  volume =       "1893",
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{Yu:1997:IAM,
  author =       "Shenwei Yu and Zhaohui Luo",
  title =        "Implementing a Model Checker for {LEGO}",
  booktitle =    "Formal Methods Europe",
  editor =       "John Fitzgerald and Cliff B. Jones and Peter Lucas",
  volume =       "1313",
  series =       "LNCS",
  publisher =    "Springer",
  year =         "1997",
  pages =        "442--458",
}


@InProceedings{Sprenger:1998:AVM,
  author =       "Christoph Sprenger",
  title =        "A Verified Model Checker for the Modal
                  $\mu$-Calculus in {Coq}",
  booktitle =    "TACAS",
  pages =        "167--183",
  year =         "1998",
  editor =       "B. Steffen",
  volume =       "1384",
  series =       "LNCS",
  publisher =    "Springer"
}

@TechReport{Wang:2005:PFM,
  author =       "Bow-Yaw Wang",
  title =        "Proving $\forall\mu$-Calculus Properties with
                  {SAT}-based Model Checking",
  institution =  "Institute of Information Science, Academia Sinica",
  year =         "2005",
  number =       "TR-IIS-05-003",
  note =          "http://www.iis.sinica.edu.tw/LIB/TechReport/tr2005/tr05003.pdf",
}

@inproceedings{Clarke:1994:ALL,
  author =       "E. Clarke and O. Grumberg and K. Hamaguchi",
  title =        "Another Look at {LTL} Model Checking",
  series =       "LNCS",
  booktitle =    "Computer Aided Verification",
  volume =       "818",
  editor =       "D. L. Dill",
  pages =        "415--428",
  year =         "1994",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
  publisher =    "Springer",
  acknowledgement = ack-nhfb,
}

@Article{Basin:2004:RMF,
  author =       "David Basin and Manuel Clavel and Jos{\'e} Meseguer",
  title =        "Reflective metalogical frameworks",
  journal =      "ACM Transactions on Computational Logic",
  volume =       "5",
  number =       "3",
  pages =        "528--576",
  month =        jul,
  year =         "2004",
  CODEN =        "????",
  ISSN =         "1529-3785",
  bibdate =      "Thu Nov 4 07:59:49 MST 2004",
  acknowledgement = ack-nhfb,
}

@InProceedings{Basin-Clavel-Meseguer99,
  author =       "David Basin and Manuel Clavel and Jos{\'e} Meseguer",
  title =        "Reflective Metalogical Frameworks",
  booktitle =    "Proceedings of LFM'99: Workshop on Logical Frameworks
                 and Meta-languages",
  address =      "Paris, France",
  month =        "September",
  year =         "1999",
}

@Unpublished{Wang:2004:UMC,
  author =       "Bow-Yaw Wang",
  title =        "Unbounded Model Checking with {SAT} - a Local Model
                  Checking Approach",
  year =         "2004",
  note =         "unpublished manuscript",
}

@Unpublished{Schuele:2005:BLM,
  author =       "Tobias Schuele and Klaus Schneider",
  title =        "Bounded Local Model Checking",
  year =         "2005",
  note =         "private communication",
}

@InProceedings{Schuele:2004:GLM,
  author =       "Tobias Schuele and Klaus Schneider",
  title =        "Global vs. Local Model Checking: A Comparison of
                  Verification techniques for Infinite State Systems",
  booktitle =    "International Conference on Software Engineering and
                  Formal Methods (SEFM)",
  year =         "2004",
  address =      "Beijing",
  month =        "Septempber",
  publisher =    "IEEE Computer Society Press",
}

@Article{Dong:2002:VCM,
  author =       "Yifei Dong and Beata Sarna-Starosta and Ramakrishnan
                 Ramakrishnan and Scott A. Smolka",
  title =        "Vacuity Checking in the Modal Mu-Calculus",
  journal =      "Lecture Notes in Computer Science",
  volume =       "2422",
  pages =        "147--??",
  year =         "2002",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Tue Sep 10 19:10:23 MDT 2002",
  URL =          "http://link.springer-ny.com/link/service/series/0558/bibs/2422/24220147.htm;
                 http://link.springer-ny.com/link/service/series/0558/papers/2422/24220147.pdf",
  acknowledgement = ack-nhfb,
}

@Article{Kupferman:2003:VDT,
  author =       "Orna Kupferman and Moshe Y. Vardi",
  title =        "Vacuity detection in temporal model checking",
  journal =      "International Journal on Software Tools for Technology
                 Transfer (STTT)",
  volume =       "4",
  number =       "2",
  pages =        "224--233",
  month =        feb,
  year =         "2003",
  CODEN =        "????",
  ISSN =         "1433-2779 (print), 1433-2787 (electronic)",
  bibdate =      "Tue Nov 23 15:01:41 MST 2004",
  acknowledgement = ack-nhfb,
  doi =          "10.1007/s100090100062",
}

@Article{Ball:2001:APA,
  author =       "Thomas Ball and Rupak Majumdar and Todd Millstein and
                 Sriram K. Rajamani",
  title =        "Automatic Predicate Abstraction of {C} Programs",
  journal =      "ACM SIG{\-}PLAN Notices",
  volume =       "36",
  number =       "5",
  pages =        "203--213",
  month =        may,
  year =         "2001",
  CODEN =        "SINODQ",
  ISSN =         "0362-1340",
  bibdate =      "Sun Dec 14 09:18:26 MST 2003",
  acknowledgement = ack-nhfb,
}


@Manual{Coq,
  title =        "The Coq Proof Assistant Reference Manual: version 8.0",
  author =       "{The Coq Development Team}",
  organization = "LogiCal Project",
  year =         "2004",
}

@TechReport{HueKahPau97,
  author =       "G{\'e}rard Huet and Gilles Kahn and Paulin-Mohring",
  institution =  "Institut National de Recherche en Informatique et en
                 Automatique",
  number =       "204",
  title =        "The {Coq} proof assistant: a tutorial: version 6.1",
  type =         "Technical Report",
  year =         "1997",
  crindex =      "Fichier",
  URL =          "ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RT/RT-0204.pdf",
}

@Book{Isabelle,
  author =     "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
  title =      "Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
  publisher =    "Springer",
  year =         "2002",
  volume =       "2283",
  series =       "LNCS",
}

@Manual{Melh90,
  author =       "T. F. Melham",
  key =          "Melh90",
  keyword =      "formalism higher-order logic HOL tutorial",
  organization = "University of Cambridge, Computer Laboratory",
  title =        "Introduction to the {HOL} theorem prover",
  year =         "1990",
}

@Article{BoMo84,
  author =       "{R.S. Boyer} and {J.S. Moore}",
  journal =      "Contemporary Mathematics",
  key =          "BoMo84",
  pages =        "119--132",
  title =        "Proof-Checking Theorem-Proving and Program
                 Verification",
  volume =       "29",
  year =         "1984",
}

@Book{Mitchell1997,
  author =       "Tom M. Mitchell",
  title =        "Machine Learning",
  publisher =    "McGraw-Hill",
  address =      "New York",
  keywords =     "machine learning, honours reading",
  year =         "1997",
}

@Article{Lamport:1994:VSC,
  author =       "L. Lamport",
  title =        "Verification and Specification of Concurrent
                 Programs",
  journal =      "Lecture Notes in Computer Science",
  volume =       "803",
  pages =        "347--??",
  year =         "1994",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Mon May 13 11:52:14 MDT 1996",
  acknowledgement = ack-nhfb,
}

@Article{ClarkeWing96,
  author =       "Edmund Clarke and Jeanette M. Wing",
  title =        "Formal Methods: State of the Art and Future
                 Directions",
  journal =      "ACM Computing Surveys",
  volume =       "28",
  number =       "4",
  pages =        "626--643",
  year =         "1996",
}

@InProceedings{DAC97*258,
  author =       "Robert P. Kurshan",
  title =        "Formal Verification in a Commercial Setting",
  pages =        "258--262",
  booktitle =    "DAC",
  month =        jun # " ~9--13",
  publisher =    "ACM Press",
  year =         "1997",
}

@Article{Oncina92,
  author =       "J. Oncina and P. Garci",
  title =        "Inferring regular languages in polynomial updated
                 time.",
  journal =      "Pattern Recognition: 4th Spanish Symp.",
  pages =        "49--61",
  publisher =    "World Scientific",
  year =         "1992",
  keywords =     "conf, infer, finite state, FSA, FSM, grammar,
                 language, learn, learning",
  abstract =     "from R a m a n' s thesis '97",
}

@Article{delaHiguera:2004:ILP,
  author =       "C. de la Higuera and J. C. Janodet",
  title =        "Inference of $\omega$-languages from prefixes",
  journal =      "Theoretical Computer Science",
  volume =       "313",
  number =       "2",
  pages =        "295--312",
  day =          "17",
  month =        feb,
  year =         "2004",
  CODEN =        "TCSCDI",
  ISSN =         "0304-3975",
  bibdate =      "Mon Feb 9 08:35:35 MST 2004",
  acknowledgement = ack-nhfb,
}

@Article{Gold67,
  author =       "E. M. Gold",
  title =        "Language identification in the limit.",
  journal =      "Information and Control",
  volume =       "10",
  pages =        "447--474",
  year =         "1967",
  keywords =     "inductive inference, II, ML, machine learning,
                 language, AI, grammar, rule rules",
  abstract =     "from refs in previous entry",
}


@InCollection{manolios00,
  author =    "Panagiotis Manolios",
  booktitle =    "Computer-Aided Reasoning: ACL2 Case Studies",
  title =        "Mu-Calculus Model-Checking",
  publisher =    "Kluwer Academic Publishers",
  year =         "2000",
  month =        "June",
  pages =        "93--111",
}

@inproceedings{verma00reflecting,
    author = "Kumar Neeraj Verma and Jean {Goubault-Larrecq} and
                  Sanjiva Prasad and S. {Arun-Kumar}",
    title = "Reflecting {BDD}s in {C}oq",
    booktitle = "Proc.\ 6th Asian Computing Science Conference
                  ({ASIAN}'2000), Penang, Malaysia, Nov. 2000",
    volume = "1961",
    publisher = "Springer",
    pages = "162--181",
    year = "2000",
    url = "citeseer.ist.psu.edu/verma00reflecting.html" }

@InProceedings{Shoham-Grumberg04,
  author =       "Sharon Shoham and Orna Grumberg",
  title =        "Monotonic Abstraction-Refinement for CTL",
  booktitle =    "Tools and Algorithms for the Construction and
                  Analysis of Systems",
  pages =     "546-560",
  year =      "2004",
  editor =    "K. Jensen and A. Podelski",
  volume =    "2988",
  series =    "LNCS",
  publisher = "Springer",
}

@InProceedings{Reps-Sagiv-Wilhelm04,
  author =       "Thomas W. Reps and Mooly Sagiv and Reinhard Wilhelm",
  title =        "Static Program Analysis via 3-Valued Logic",
  booktitle =    "Computer Aided Verification",
  pages =        "15-30",
  year =      "2004",
  editor =    "R. Alur and D.A. Peled",
  volume =    "3114",
  series =    "LNCS",
  publisher = "Springer",
}

@Article{Schuppan-Biere04,
  author =       "V. Schuppan and A. Biere",
  title =        "Efficient Reduction of Finite State Model Checking
                  to Reachability Analysis",
  journal =      "Software Tools for Technology Transfer",
  year =         "2004",
  volume =       "5",
  number =       "2-3",
  pages =        "185-204",
  month =        "March",
  publisher =    "Springer",
}

@InProceedings{Clarke-Kroening-Ouaknine-Strichman04,
  author =       "E. Clarke and D. Kroening and J. Ouaknine and O. Strichman",
  title =        "Completeness and Complexity of Bounded Model Checking",
  series =       "LNCS",
  booktitle =    "VMCAI",
  volume =       "2937",
  pages =        "85--96",
  year =         "2004",
  editor =       "Bernhard Steffen and Giorgio Levi",
  publisher =    "Springer",
}

@InProceedings{Awedh-Somenzi04,
  author =       "Mohammad Awedh and Fabio Somenzi",
  title =        "Proving More Properties with Bounded Model Checking",
  series =       "LNCS",
  booktitle =    "CAV",
  volume =       "3114",
  pages =        "96--108",
  year =         "2004",
  editor =       "R. Alur and D. A. Peled",
  publisher = "Springer",
}

@InCollection{Meseguer93,
  author =       {Jos{\'e} Meseguer},
  title =        {A Logical Theory of Concurrent Objects and its
                  realization in the {Maude} Language},
  booktitle =    {Research Directions in Concurrent Object-Oriented
                  Programming},
  editor =       {Gul Agha and Peter Wegner and Akinori Yonezawa},
  year =         1993,
  pages =        {314-390},
  publisher =    mit
}

@InProceedings{Wang04,
  author =       "B.-Y. Wang",
  title =        "$\mu$-Calculus Model Checking in Maude",
  year =         "2004",
  editor =       "Narciso Mart\'i-Oliet",
  booktitle =    "5th International Workshop on Rewriting Logic and
                  its Applications",
  series =       "Electronic Notes in Theoretical Computer Science",
  volume =       "117",
  pages =        "135--152",
  publisher =    "Elsevier Science Publishers",
}

@InProceedings{Denker-Meseguer-Talcott98,
  author =       "Grit Denker and Jos{\'e} Meseguer and Carolyn L.
                 Talcott",
  title =        "Protocol Specification and Analysis in {Maude}",
  booktitle =    "Proceedings of Workshop on Formal Methods and Security
                 Protocols, June 25, 1998, Indianapolis, Indiana",
  year =         "1998",
  editor =       "N. Heintze and J. Wing",
  OPTnote =         "\url{http://www.cs.bell-labs.com/who/nch/fmsp/index.html}",
}

@PhdThesis{Scatte98,
  author =       "Bryan Scattergood",
  title =        "The Semantics and Implementation of Machine-Readable
                 {CSP}",
  added-by =     "anadel",
  URL =          "http://www.formal.demon.co.uk/papers/cspm.ps.gz",
  annote =       "Basics of machine-readable CSP, which is used by the
                 FDR-tool.",
  year =         "1998",
  added-at =     "Fri Dec 15 15:13:00 2000",
  school =       "University of Oxford",
}

@InProceedings{Baumgartner:2002:PCS,
  author =       "Jason Baumgartner and Andreas Kuehlmann and Jacob Abraham",
  title =        "Property Checking via Structural Analysis",
  journal =      "Lecture Notes in Computer Science",
  booktitle =    "Proc. of CAV",
  volume =       "2404",
  pages =        "151--??",
  year =         "2002",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
}

@InProceedings{McMillan2003,
  author =       "K. L. McMillan",
  title =        "Interpolation and {SAT}-based Model Checking",
  year =         "2003",
  editor =    "Warren A. Hunt Jr. and Fabio Somenzi",
  booktitle = "CAV",
  volume =    "2725",
  pages =     "1-13",
  series =    "LNCS",
  publisher = "Springer",
}

@InProceedings{dMRS2003,
  author =    "Leonardo de Moura, Harald Rue\ss and Maria Sorea",
  title =     "Bounded Model Checking and Induction: From Refutation to Verification",
  year =         "2003",
  editor =    "Warren A. Hunt Jr. and Fabio Somenzi",
  booktitle = "Computer Aided Verification",
  volume =    "2725",
  pages =     "14-26",
  series =    "LNCS",
  publisher = "Springer",
}

@InProceedings{Copty2001a,
  author =       "F. Copty and L. Fix and E. Giunchiglia and G. Kamhi
                 and A. Tacchella and M. Vardi",
  title =        "Benefits of Bounded Model Checking at an Industrial
                 Setting",
  booktitle =    "Proc. of CAV",
  year =         "2001",
  series =       "LNCS",
  publisher =    "Springer",
  URL =          "http://www.mrg.dist.unige.it/~sim/simo/Publications/Data/bmcsat.ps.gz",
}

@InProceedings{Biere99a,
  author =       "A. Biere and E. Clarke and R. Raimi and Y. Zhu",
  year =         "1999",
  title =        "Verifying Safety Properties of a {PowerPC}
                 Microprocessor Using Symbolic Model Checking Without
                 {BDDs}",
  booktitle =    "CAV",
  pages =        "60--71",
  publisher =    {Springer},
  series =       {LNCS},
  abstract =     "In [1] Bounded Model Checking with the aid of
                 satisfiability solving (SAT) was introduced as an
                 alternative to symbolic model checking with BDDs. In
                 this paper we show how bounded model checking can take
                 advantage of specialized optimizations. We present a
                 bounded version of the cone of influence reduction. We
                 have successfully applied this idea in checking safety
                 properties of a PowerPC microprocessor at Motorola's
                 Somerset PowerPC design center. Based on that
                 experience, we propose a verification methodology that
                 we feel can bring model checking into the mainstream of
                 industrial chip design.",
}

@InProceedings{Moskewicz2001a,
  author =       "Matthew W. Moskewicz and Conor F. Madigan and Ying
                 Zhao and Lintao Zhang and Sharad Malik",
  title =        "{Chaff: Engineering an Efficient {SAT} Solver}",
  booktitle =    "Design Automation Conference",
  year =         "2001",
  month =        jun,
  URL =          "http://www.ee.princeton.edu/~chaff/DAC2001v56.pdf",
}

@InProceedings{Zhang2001a,
  author =       "L. Zhang and C. F. Madigan and M. W. Moskewicz and S.
                 Malik",
  title =        "Efficient Conflict Driven Learning in a {B}oolean
                 Satisfiability Solver",
  booktitle =    "International Conference on Computer-Aided Design
                 (ICCAD'01)",
  month =        nov,
  year =         "2001",
  pages =        "279--285",
  URL =          "http://www.ee.princeton.edu/~chaff/iccad2001_final.pdf",
}

@Manual{CUDDManual,
  title =     "CUDD:CU Decision Diagram Package Release 2.3.1",
  author =    "Fabio Somenzi",
  organization = "Department of Electrical and Computer Engineering,
                  University of Colorado at Boulder",
  year =      "2001",
  URL =      "http://vlsi.colorado.edu/~fabio/CUDD/",
}

@Misc{OCamlManual,
  author =       "Xavier Leroy",
  title =        "The {O}bjective {C}aml System: Documentation and
                 User's Manual",
  year =         "2000",
  note =         "With Damien Doligez, Jacques Garrigue, Didier R\'emy,
                 and J\'er\^ome Vouillon.",
  URL =          "http://caml.inria.fr",
}

@Book{clarke_em-etal:1999a,
  author =       "Edmund M. Clarke and Orna Grumberg and Doron A.
                 Peled",
  title =        "Model Checking",
  publisher =    "The {MIT} Press",
  year =         "1999",
  address =      "Cambridge, Massachusetts",
  ISBN =         "0262032708",
  topic =        "model-checking;program-verification;",
}

@Inproceedings{EL:effmcf,
  author =       "E. Allen Emerson and Chin-Laung Lei",
  title =        "Efficient Model-Checking in Fragments of the
                 Propositional Mu-Calculus",
  booktitle =    "Proceedings First Annual IEEE Symposium on Logic in
                 Computer Science",
  pages =        "267--278",
  publisher =    "IEEE Computer Society Press",
  month =        "June",
  year =         "1986",
}

@InProceedings{LICS::AndersenSW1994,
  title =        "A Compositional Proof System for the Modal
                 $\mu$-Calculus",
  author =       "Henrik Reif Andersen and Colin Stirling and Glynn
                 Winskel",
  pages =        "144--153",
  booktitle =    "Proceedings, Ninth Annual {IEEE} Symposium on Logic in
                 Computer Science",
  year =         "1994",
  month =        "4--7 " # jul,
  address =      "Paris, France",
  organization = "IEEE Computer Society Press",
  references =   "\cite{LICS::EmersonL1986} \cite{IC::Winskel1990}",
}

@TechReport{Verdejo-Marti02,
  author =       "Alberto Verdejo and Narciso Mart{\'i}-Oliet",
  title =        "Executing and Verifying CCS in Maude",
  month =        "October",
  year =         "2002",
  note =         "Submitted for publication",
}

@Article{IC::BurchCMDH1992,
  title =        "Symbolic Model Checking: $10^{20}$ States and Beyond",
  author =       "J. R. Burch and E. M. Clarke and K. L. McMillan and D.
                 L. Dill and L. J. Hwang",
  pages =        "142--170",
  journal =      "Information and Computation",
  month =        jun,
  year =         "1992",
  volume =       "98",
  number =       "2",
  publisher =    "Academic Press",
  preliminary =  "LICS::BurchCMDH1990:428",
}

@Manual{Clavel-Duran-Eker03,
  title =        "Maude 2.0 Manuel",
  author =       "Manuel Clavel and Francisco Dur{\'a}n and Steven Eker and
                  Patrick Lincoln and Narciso Mart{\'i}-Oliet and
                  Jos{\'e} Meseguer and Carolyn Talcott",
  edition =      "version 1.0",
  month =        "June",
  year =         "2003",
  url =          "http://maude.cs.uiuc.edu"
}

@Article{Dam:ctlcfm-j,
  author =       "Mads Dam",
  title =        "{CTL$\star$} and {ECTL$\star$} as Fragments of the
                 Modal $\mu$-Calculus",
  journal =      "Theoretical Computer Science",
  volume =       "126",
  number =       "1",
  pages =        "77--96",
  year =         "1994",
}

@Article{ACTAI::Cleaveland1989,
  title =        "Tableau-Based Model Checking in the Propositional
                 Mu-Calculus",
  author =       "Rance Cleaveland",
  journal =      "Acta Informatica",
  pages =        "725--747",
  year =         "1989",
  volume =       "27",
  number =       "8",
  publisher =    "Springer",
}

@Article{Winskel91a,
  author =       "Glynn Winskel",
  title =        "A Note on Model Checking the Modal nu-Calculus",
  journal =      "Theoretical Computer Science",
  pages =        "157-167",
  volume =       "83",
  year =         "1991",
  publisher =    "Elsevier Science Publishers",
}

@InCollection{SW:locmcm-c,
  author =       "Colin Stirling and David Walker",
  title =        "Local Model Checking in the Modal Mu-Calculus",
  editor =       "J. D{\'i}az and F. Orejas",
  booktitle =    "Proceedings Int.\ Joint Conf.\ on Theory and Practice
                 of Software Development",
  series =       "LNCS",
  volume =       "351",
  pages =        "369--383",
  publisher =    "Springer",
  address =      "Berlin",
  year =         "1989",
}

@InProceedings{Eker-Meseguer-Sridharanarayanan02,
  author =       "Steven Eker and Jos{\'e} Meseguer and
                  Ambarish Sridharanarayanan",
  title =        "The {Maude} {LTL} Model Checker",
  series =       "Electronic Notes in Theoretical Computer Science",
  volume =       "71",
  booktitle =    "Proceedings of the Fourth International Workshop on
                  Rewriting Logic",
  year =         "2002",
  organization = "Elsevier Science Publishers",
  OPTurl =          "http://www.elsevier.nl/locate/entcs/volume71.html"
}

@InProceedings{Wang-Meseguer-Gunter00,
  author =       "Bow-Yaw Wang and Jos{\'e} Meseguer and Carl A.
                 Gunter",
  title =        "Specification and formal analysis of a {PLAN}
                 algorithm in {Maude}",
  booktitle =    "Proceedings International Workshop on Distributed
                 System Validation and Verification",
  editor =       "Pao-Ann Hsiung",
  month =        apr,
  year =         "2000",
  pages =        "49--56",
}

@Article{Marti-Oliet:2002:RLR,
  author =       "Narciso Mart{\'\i}-Oliet and Jos{\'e} Meseguer",
  title =        "Rewriting logic: roadmap and bibliography",
  journal =      "Theoretical Computer Science",
  volume =       "285",
  number =       "2",
  pages =        "121--154",
  month =        aug,
  year =         "2002",
  coden =        "TCSCDI",
  ISSN =         "0304-3975",
  publisher =    "Elsevier Science Publishers",
  bibdate =      "Wed Nov 20 18:08:58 MST 2002",
  acknowledgement = ack-nhfb,
}

@Article{Meseguer:1992:CRL,
  author =       "J. Meseguer",
  title =        "Conditional rewriting logic as a unified model of
                 concurrency",
  journal =      "Theoretical Computer Science",
  volume =       "96",
  number =       "1",
  pages =        "73--155",
  day =          "06",
  month =        apr,
  year =         "1992",
  coden =        "TCSCDI",
  ISSN =         "0304-3975",
  bibdate =      "Sat Nov 22 13:24:22 MST 1997",
  acknowledgement = ack-nhfb,
  classification = "C4210 (Formal logic); C6110J (Object-oriented
                 programming); C6110P (Parallel programming)",
  conflocation = "San Miniato, Italy; 28 Feb.-3 March 1990",
  conftitle =    "2nd Workshop on Concurrency and Compositionality",
  corpsource =   "SRI Int., Menlo Park, CA, USA",
  pubcountry =   "Netherlands",
  treatment =    "B Bibliography; P Practical",
  xxtitle =      "Conditioned rewriting logic as a unified model of
                 concurrency",
}

@InProceedings{Clavel96,
  author =       "Manuel Clavel and Steven Eker and Patrick Lincoln and
                 Jos\'e Meseguer",
  title =        "Principles of {M}aude",
  editor =       "Jos\'e Meseguer",
  volume =       "4",
  series =       "Electronic Notes in Theoretical Computer Science",
  pages =        "65--89",
  booktitle =    "Proceedings of the First International Workshop on
                 Rewriting Logic",
  year =         "1996",
  organization = "Elsevier Science Publishers",
  OPTurl =          "http://www.csl.sri.com/~clavel/pubs/rwl96b.ps",
}

@InProceedings{CONCUR::Meseguer1996,
  title =        "Rewriting Logic as a Semantic Framework for
                  Concurrency: {A} Progress Report",
  author =       "Jos{\'e} Meseguer",
  pages =        "331--372",
  booktitle =    "CONCUR~'96: Concurrency Theory, 7th International
                 Conference",
  editor =       "Ugo Montanari and Vladimiro Sassone",
  year =         "1996",
  series =       "LNCS",
  volume =       "1119",
  publisher =    "Springer",
  ISBN =         "ISBN 3-540-61604-7",
}

@InProceedings{Meseguer00-rta,
  author =       "Jos{\'e} Meseguer",
  title =        "Rewriting Logic and {Maude}: Concepts and
                 Applications",
  booktitle =    "Rewriting Techniques and Applications, 11th
                 International Conference",
  editor =       "L. Bachmair",
  pages =        "1--26",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       "1833",
  year =         "2000",
}

@InProceedings{Clavel98,
  author =       "Manuel Clavel",
  title =        "Reflection in General Logics, Rewriting Logic, and
                 {Maude}",
  pages =        "317--328",
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  booktitle =    "Proceedings Second International Workshop on Rewriting
                  Logic and its Applications",
  year =         "1998",
  publisher =    "Elsevier Science Publishers",
  volume =       "15",
  series =       "Electronic Notes in Theoretical Computer Science",
  OPTnote =         "http://www.elsevier.nl/locate/entcs/volume15.html",
}

@InProceedings{Clavel-Meseguer96-wrla,
  author =       "Manuel Clavel and Jos{\'e} Meseguer",
  title =        "Reflection and strategies in rewriting logic",
  booktitle =    "Proceedings First International Workshop on Rewriting
                 Logic and its Applications",
  year =         "1996",
  editor =       "Jos{\'e} Meseguer",
  publisher =    "Elsevier Science Publishers",
  volume =       "4",
  pages =        "125--147",
  series =       "Electronic Notes in Theoretical Computer Science",
  OPTnote =         "http://www.elsevier.nl/locate/entcs/volume4.html",
}

@InProceedings{Carabetta-Degano-Gadducci98,
  author =       "Georgia Carabetta and Pierpaolo Degano and Fabio
                 Gadducci",
  title =        "{CCS} Semantics via Proved Transition Systems and
                 Rewriting Logic",
  pages =        "253--272",
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  booktitle =    "Proceedings Second International Workshop on Rewriting
                 Logic and its Applications, WRLA'98, Pont-\`a-Mousson,
                 France, September 1--4, 1998",
  year =         "1998",
  publisher =    "Elsevier Science Publishers",
  volume =       "15",
  series =       "Electronic Notes in Theoretical Computer Science",
  OPTnote =         "http://www.elsevier.nl/locate/entcs/volume15.html",
}


@InProceedings{Basin:2000:RLM,
  author =       "David Basin and Manuel Clavel and Jos{\'e} Meseguer",
  title =        "Rewriting Logic as a Metalogical Framework",
  booktitle =    "The 20th Conference on Foundations of Software Technology and Theoretical Computer Science",
  series =      "LNCS",
  volume =       "1974",
  editor =       "Sanjiv Kapoor	and Sanjiva Prasad",
  pages =        "55--80",
  year =         "2000",
  coden =        "LNCSD9",
  ISSN =         "0302-9743",
  publisher =    "Springer",
}

@Misc{VISBenchmark,
  key =       "{VIS} Verification Benchmarks",
  title =     "VIS Verification Benchmarks",
  url =          "ftp://vlsi.colorado.edu/pub/vis/vis-verilog-models-1.0.tar.gz"
}

@Misc{USBphy,
  author =    "R. Usselmann",
  title =     "USB 1.1 PHY Project",
  url =       "http://www.opencores.org/projects/usb_phy/",
}

@Unpublished{BWang:2002:patent,
  author =       "B.-Y. Wang",
  title =        "BDD and Inductive Proof",
  note =         "manuscript. Verplex Systems, Inc",
  year =         "2002",
  OPTannote =    {}
}

@InProceedings{DAC99*317,
  author =       "A. Biere and A. Cimatti and E. M. Clarke and M. Fujita
                 and Y. Zhu",
  title =        "Symbolic Model Checking using {SAT} Procedures Instead
                 of {BDDs}",
  pages =        "317--320",
  booktitle =    "DAC",
  ISBN =         "1-58113-092-9",
  month =        jun,
  publisher =    "ACM Press",
  year =         "1999",
}

@InProceedings{BCCZ99,
  author =       "Armin Biere and Alessandro Cimatti and Edmund Clarke
                 and Yunshan Zhu",
  title =        "Symbolic Model Checking without {BDDs}",
  series =       "LNCS",
  volume =       "1579",
  pages =        "193--207",
  year =         "1999",
  editor =       "W. R. Cleaveland",
  booktitle =    "TACAS",
  publisher =    "Springer",
}

@InProceedings{Maidl:2000:CFC,
  author =       "M. Maidl",
  title =        "The common fragment of {CTL} and {LTL}",
  editor =       "{IEEE}",
  booktitle =    "41st Annual Symposium on Foundations of Computer
                 Science: proceedings: 12--14 November, 2000, Redondo
                 Beach, California",
  publisher =    "IEEE Computer Society Press",
  address =      "1109 Spring Street, Suite 300, Silver Spring, MD
                 20910, USA",
  year =         "2000",
  ISBN =         "0-7695-0850-2, 0-7695-0851-0 (case), 0-7695-0852-9
                 (microfiche)",
  pages =        "643--652",
  bibdate =      "Thu Apr 5 06:14:11 MDT 2001",
  acknowledgement = ack-nhfb,
}

@InProceedings{Forspec02,
  author =       "Roy Armoni and Limor Fix and Alon Flaisher and Rob
                 Gerth and Boris Ginsburg and Tomer Kanza and Avner
                 Landver and Sela Mador-Haim and Eli Singerman and
                 Andreas Tiemeyer and Moshe Y. Vardi and Yael Zbar",
  title =        "The {ForSpec} Temporal Logic: {A} New Temporal
                 Property Specification Language",
  series =       "LNCS",
  volume =       "2280",
  pages =        "296--311",
  publisher =    "Springer",
  editor =       "Joost-Pieter Katoen and Perdita Stevens",
  booktitle =    "TACAS",
  year =         "2002",
}

@Article{TCS::BrowneCJLM1997,
  title =        "An improved algorithm for the evaluation of fixpoint
                 expressions",
  author =       "A. Browne and E. M. Clarke and S. Jha and D. E. Long
                 and W. Marrero",
  pages =        "237--255",
  journal =      "Theoretical Computer Science",
  month =        "30~" # may,
  year =         "1997",
  volume =       "178",
  number =       "1--2",
  references =   "\cite{IPL::ArnoldC1988} \cite{LICS::BurchCMDH1990}
                 \cite{TOPLAS::ClarkeES1986}
                 \cite{ACTAI::Cleaveland1989} \cite{LICS::EmersonL1986}
                 \cite{JCSS::FischerL1979} \cite{TCS::Kozen1983}
                 \cite{TCS::StirlingW1991}",
}

@InProceedings{ICCD99*467,
  author =       "K. Ravi and F. Somenzi",
  title =        "Efficient Fixpoint Computation for Invariant
                 Checking",
  pages =        "467--475",
  booktitle =    "International Conference on Computer Design ({ICCD}
                 '99)",
  ISBN =         "0-7695-0406-X",
  month =        oct,
  publisher =    "IEEE",
  address =      "Washington - Brussels - Tokyo",
  year =         "1999",
}

@InProceedings{vanEijk:1998:SEC,
  author =       "C. A. J. van Eijk",
  title =        "Sequential Equivalence Checking Without State Space Traversal",
  booktitle =    "Proceedings of the Design, Automation and Test in Europe",
  pages =     "618-623",
  year =      "1998",
  address =   "Le Palais des Congr\'s de Paris, France",
  month =     "Feburary",
}

@Article{Bjesse:2000:SBV,
  author =       "Per Bjesse and Koen Claessen",
  title =        "{SAT}-Based Verification without State Space
                 Traversal",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1954",
  pages =        "372--??",
  year =         "2000",
  coden =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Tue Sep 10 19:08:55 MDT 2002",
  url =          "http://link.springer-ny.com/link/service/series/0558/bibs/1954/19540372.htm;
                 http://link.springer-ny.com/link/service/series/0558/papers/1954/19540372.pdf",
  acknowledgement = ack-nhfb,
}

@inproceedings{Sheeran:2000:CSP,
  author =       "Mary Sheeran and Satnam Singh and Gunnar
                 St{\aa}lmarck",
  title =        "Checking Safety Properties Using Induction and a
                 {SAT}-Solver",
  series =       "LNCS",
  volume =       "1954",
  pages =        "108--125",
  year =         "2000",
  coden =        "LNCSD9",
  editor =       "Warren A. Hunt Jr. and Steven D. Johnson",
  booktitle =    "Formal Methods in Computer-Aided Design",
  ISSN =         "0302-9743",
  publisher =    "Springer",
}

@InProceedings{1999:fm:a:deharbe,
  author =       "David D{\'e}harbe and Anamaria Martins Moreira",
  title =        "Symbolic Model Checking with Fewer Fixpoint
                 Computations",
  editor =       "Jeanette M. Wing and Jim Woodcock and Jim Davies",
  booktitle =    "{FM}'99---Formal Methods, Volume~{I}",
  year =         "1999",
  volume =       "1708",
  series =       "LNCS",
  publisher =    "Springer",
  pages =        "272--288",
  annote =       "incomplete",
}

@Book{Mitchell96,
  author = 	 {John C. Mitchell},
  title = 	 {Foudations for Programming Languages},
  publisher = 	 {The MIT Press},
  year = 	 {1996},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {Foundations of Computing},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Manual{DHCP,
  title = 	 "Dynamic Host Configuration Protocol",
  OPTkey = 	 {},
  author = 	 "R. Droms",
  OPTorganization = "Computer Science Department, Bucknell University",
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month = 	 "March",
  year = 	 "1997",
  note = 	 "RFC 2131",
  OPTannote = 	 {}
}

@Manual{PPP,
  title = 	 "The Point-to-Point Protocol",
  OPTkey = 	 {},
  author = 	 "W. Simpson",
  organization = "Computer Systems Consulting Services",
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month = 	 "July",
  year = 	 "1994",
  note = 	 "STD 51, RFC 1661",
  OPTannote = 	 {}
}

@inproceedings{
AbadiHalpern,
        author="M. Abadi and J.Y. Halpern",
	title="Decidability and expressiveness for first-order logics of
  		probability",
	booktitle="Proceedings of the 30th  IEEE Symposium on
         	Foundations of Computer	Science",
        year="1989"
	}

	@inproceedings{
AggarwalKurshan,
	author="S. Aggarwal and R.P. Kurshan",
	title="Modeling elapsed time in Protocol Specification",
	booktitle="IFIP Protocol Specification, Testing, and Verification",
	year="1983",
	volume="III",
	pages="51-62",
	editor="H. Rudin and C.H. West"
	}

	@inproceedings{
AKS,
	author="S. Aggarwal and R.P. Kurshan and K. Sabnani",
	title="A calculus for protocol specification and validation",
	booktitle="IFIP Protocol Specification, Testing, and Verification",
	year="1983",
	volume="III",
	pages="19-34",
	editor="H. Rudin and C.H. West"
	}


	@inproceedings{
AKS83,
	author="S. Aggarwal and R.P. Kurshan and D. Sharma",
	title="A language for the specification and analysis of protocols",
	booktitle="IFIP Protocol Specification, Testing, and Verification",
	year="1983",
	volume="III",
	pages="35-50",
	editor="H. Rudin and C.H. West"
	}
	

	@article{
AlpernSchneider,
	author="B. Alpern and F.B. Schneider",
	title="Verifying temporal properties without using temporal logic",
	year="1989",
	volume="11",
	number="1",
	journal="ACM Transactions on Programming Languages and Systems",
	pages="147-167"
	}

	@article{
TCTL,
        author="R. Alur and C. Courcoubetis and D.L. Dill",
	title="Model-checking in dense real-time",
	journal="Information and Computation",
	year="1993",
	volume="104",
	number="1",
	pages="2-34",
	}

	@inproceedings{
PTCTL,
	title="Model-checking for probabilistic real-time systems",
	author="R. Alur and C. Courcoubetis and D.L. Dill",
	booktitle="Automata, Languages and Programming:
		Proceedings of the 18th ICALP",
	series="LNCS",
        volume="510",
	publisher={Springer},
	pages="115-136",
	year="1991",
	}

	@inproceedings{
REXpaper,
	title="Verifying automata specifications of
		probabilistic real-time systems",
	author="R. Alur and C. Courcoubetis and D.L. Dill",
	booktitle={Real-Time: Theory in Practice, REX Workshop},
	series="LNCS",
        volume="600",
	pages="28-44",
	publisher="Springer",
	year="1991"
	}

	@inproceedings{
REXsurvey,
	title="Logics and Models of Real Time: A Survey",
	author="R. Alur and T.A. Henzinger",
	booktitle={Real-Time: Theory in Practice, REX Workshop},
	series="LNCS",
        volume="600",
	publisher="Springer",
	pages="74-106",
	year="1991"
	}
		

	@incollection{
TimedAutomataO,
        author="R. Alur and D.L. Dill",
	title="Automata for modeling real-time systems",
	booktitle="Automata, Languages and Programming:
		Proceedings of the 17th ICALP",
	series="LNCS",
        volume="443",
	pages="322-335",
	publisher="Springer",
        year="1990"}

@article{
TimedAutomata,
author="R. Alur and D.L. Dill",
title="A theory of timed automata",
journal={Theoretical Computer Science},
year={1994},
volume={126},
pages="183-235"
}



	@inproceedings{
TPTLo,
        author="R. Alur and T.A. Henzinger",
	title="A really temporal logic",
	booktitle="Proceedings of the 30th IEEE Symposium on
        	Foundations of Computer	Science",
	pages="164-169",
        year="1989",
	}

@article{
TPTL,
author="R. Alur and T.A. Henzinger",
title="A really temporal logic",
journal={Journal of the ACM},
year={1994},
volume={41},
number={1},
pages={181-204}}

	@inproceedings{
BackToFuture,
        author="R. Alur and T.A. Henzinger",
	title="Back to the future: Towards a theory of timed regular languages",
	booktitle="Proceedings of the 33rd IEEE Symposium on
        	Foundations of Computer	Science",
        year="1992",
	pages="177-186"
	}

	@inproceedings{
Parametric,
	author="R. Alur and T.A. Henzinger and M.Y. Vardi",
	title="Parametric real-time reasoning",
	booktitle="Proceedings of the 25th ACM Symposium on
		Theory of Computing",
	year="1993",
	pages="592-601"
	}

	@article{
Logic,
        author="R. Alur and T.A. Henzinger",
	title="Real-time logics: complexity and expressiveness",
	journal="Information and Computation",
	year="1993",
	volume="104",
	number="1",
	pages="35-77",
	}

	@inproceedings{
MITLo,
        author="R. Alur and T. Feder and T.A. Henzinger",
	title="The benefits of relaxing punctuality",
	booktitle="Proceedings of the Tenth  ACM Symposium on
        	Principles of Distributed Computing",
	pages="139-152",
        year="1991"
	}

        @article{MITL,
        author="R. Alur and T. Feder and T.A. Henzinger",
	title="The benefits of relaxing punctuality",
	journal={Journal of the ACM},
	pages={116-146},
	volume=43,
	number=1,
        year="1996"
	}


@inproceedings{
PODC94o,
author="R. Alur and G. Taubenfeld",
title="Contention-free complexity of shared memory algorithms",
	booktitle="Proceedings of the 13th  ACM Symposium on
        	Principles of Distributed Computing",
pages={61-70},
        year="1994"
	}

		  @article{
PODC94,
author="R. Alur and G. Taubenfeld",
title="Contention-free complexity of shared memory algorithms",
	journal={Information and Computation},
pages={62-73},
        year="1996",
	volume=126,
		  number=1
	}



	@inproceedings{
BKP,
	author="H. Barringer and R. Kuiper and A. Pnueli",
	title="A really abstract concurrent model and its temporal logic",
	booktitle="Proceedings of the 13th ACM Symposium on
	Principles of Programming Languages",
        year="1986",
	pages="173--183"
	}


	@article{
BMP,
        author="M. Be{n-Ar}i and Z. Manna and A. Pnueli",
	title="The temporal logic of branching time",
	journal="Acta Informatica",
	volume="20",
	pages="207-226",
        year="1983"
	}

	@inproceedings{
BernsteinHarter,
        author="A. Bernstein and P.K. Harter",
	title="Proving real-time properties of programs with temporal logic",
	booktitle="Proceedings of the Eighth ACM Symposium on
        	Operating System Principles",
	pages="164-176",
        year="1981"
	}


	@article{
BCDM,
	author = "M.C. Browne and E.M. Clarke and D.L. Dill and
		B. Mishra",
	title = "Automatic Verification of Sequential Circuits Using
		Temporal Logic",
	Journal = "IEEE Transactions on Computers",
	Volume = "C-35",
	Number = "12",
	pages="1035-1044",
	Year = 1986
	}

	@inproceedings{
Buchi,
        author="J.R. B{\"u}chi",
	title="On a decision method in restricted second-order arithmetic",
	booktitle="Proceedings of the International Congress on Logic,
		Methodology, and Philosophy of Science 1960",
	publisher="Stanford University Press",
        year="1962",
	pages="1-12"
	}

	@incollection{
Burch,
	author="J.R. Burch",
	title="Combining {CTL}, trace theory and timing models",
	booktitle="Automatic Verification Methods for Finite State Systems:
		Proceedings of the First CAV",
	series="LNCS",
        volume="407",
	publisher="Springer",
	pages="197-212",
	year="1989"
	}

	@article{
Choueka,
	author="Y. Choueka",	
	title="Theories of automata on $\omega$-tapes: a simplified approach",
	journal="Journal of Computer and System Sciences",
	volume="8",
	year="1974",
	pages="117-141"
	}

	@techreport{
CDK,
	author="E.M. Clarke and I.A. Draghicescu and R.P. Kurshan",
	title="A unified approach for showing language containment and
		equivalence between various types of $\omega$-automata",
	institution="Carnegie Mellon University",
	year="1989"
	}

	@article{
CES,
        author="E.M. Clarke and E.A. Emerson and A.P. Sistla",
	title="Automatic verification of finite-state concurrent systems
		using temporal-logic specifications",
	journal="ACM Transactions on Programming Languages and Systems",
        volume="8",
	number="2",
        year="1986",
	pages="244-263"
        }

	@article{
Emerson83,
	author="E.A. Emerson",
	title="Alternative semantics for temporal logics",
	journal="Theoretical Computer Science",
	volume="26",
	pages="121-130",
	year="1983"
	}

	@article{
CoolahanRoussopoulos,
	author="J.E. Coolahan and N. Roussopoulos",
	title="Timing requirements for time-driven systems using
		augmented {P}etri-nets",
	journal="IEEE Transactions on Software Engineering",
	volume="SE-9",
	number="9",
	pages="603-616",
	year="1983"
	}

	@inproceedings{
DillWongToi,
	author="D.L. Dill and H. Won{g-T}oi",
 	title="Synthesizing processes and schedulers from temporal
		specifications",
        booktitle="Computer-Aided Verification, 2nd International Conference, CAV'90",
	publisher={Springer},
	series="LNCS 531",
	pages="272-281",
        year="1990"
	}
	
	@inproceedings{
BFH,
	author="A. Bouajjani and J.C. Fernandez and N. Halbwachs",
 	title="Minimal model generation",
        booktitle="Computer-Aided Verification, 2nd International Conference, CAV'90",
	publisher={Springer},
	series="LNCS 531",
	pages="197-203",
        year="1990"
	}

	@InProceedings{
Dill,
	Title="Timing assumptions and verification of finite-state
		concurrent systems",
	Author = "D.L. Dill",
	Booktitle = "Automatic Verification Methods for Finite State Systems",
	Year = "1989",
	Editor = "J. Sifakis",
	Publisher = "Springer-",
	series="LNCS 407",
	pages="197-212"
	}

	@book{
DillThesis,
	Author = "D.L. Dill",
	Title = "Trace Theory for Automatic Hierarchical Verification of
		Speed-independent Circuits",
	Publisher = "MIT Press",
series={ACM Distinguished Dissertation Series},
	Year = "1989"}

	@article{
EmersonClarke,
        author="E.A. Emerson and E.M. Clarke",
	title="Using branching-time temporal logic to synthesize
        	synchronization skeletons",
	journal="Science of Computer Programming",
        volume="2",
        year="1982",
	pages="241-266",
        publisher="Elsevier Science Publishers",
        }

	@inproceedings{
EmersonLei,
        author="E.A. Emerson and C.L. Lei",
	title="Modalities for Model-Checking: Branching time logic
		strikes back",
	booktitle="Proceedings of the 12th  ACM Symposium on
		Principles of Programming Languages",
        year="1985",
	pages="84-96",
        publisher="ACM Press",
	}

	@inproceedings{
EMSS,
	author="E.A. Emerson and A.K. Mok and A.P. Sistla
	        and J. Srinivasan",
 	title="Quantitative temporal reasoning",
        booktitle="Computer-Aided Verification, 2nd International Conference, CAV'90",
	publisher={Springer},
	series="LNCS 531",
	pages="136-145",
        year="1990"
	}


	@book{
Enderton,
	author="H. Enderton",
	title="A Mathematical Introduction to Logic",
  	publisher="Academic Press",
	year="1972"
	}

	@inproceedings{
GPSS,
        author="D. Gabbay and A. Pnueli and S. Shelah and
		J. Stavi",
	title="On the temporal analysis of fairness",
	booktitle="Proceedings of the Seventh ACM Symposium on
		Principles of Programming Languages",
        year="1980"
	}

	@inproceedings{
GodefroidWolper,
	author="P. Godefroid and P. Wolper",
 	title="A Partial Approach to Model-checking",
	Booktitle="Proceedings of the Sixth  IEEE Symposium
		on Logic in Computer Science",
	pages="406-415",
	year="1991"
	}

	@article{
HPS,
	author="D. Harel and A. Pnueli and J. Stavi",
	title="Propositional Dynamic Logic of Regular Programs",
	journal="Journal of Computer and System Sciences",
	year="1983",
	volume="26",
	pages="222-243"
	}

	@mastersthesis{
Harel,
	author="E. Harel",
	title="Temporal Analysis of Real-time Systems",
        school="The Weizmann Institute of Science",
	address="Rehovot, Israel",
        year="1988"
	}

	@inproceedings{
HLP,
        author="E. Harel and O. Lichtenstein and A. Pnueli",
	title="Explicit-clock temporal logic",
	booktitle="Proceedings of the Fifth  IEEE Symposium on
	        Logic in Computer Science",
        year="1990",
	pages="402-413"
	}

	@article{
HarelKurshan,
	author="Z. Har'El and R.P. Kurshan",
	title="Software for Analytical Development of Communication Protocols",
	journal="AT\&T Technical Journal",
	year="1990"
	}

	@article{
Kurshan,
	author="R.P. Kurshan",
	title="Complementing deterministic {B\"{u}chi} automata in
	polynomial time",
	journal="Journal of Computer and System Sciences",
	year="1987",
	volume="35",
	pages="59-71"
	}


	@inproceedings{
Henzinger,
        author="T.A. Henzinger",
	title="Half-order modal logic: how to prove real-time properties",
	booktitle="Proceedings of the Ninth  ACM Symposium on
        	Principles of Distributed Computing",
	pages="281-296",
        year="1990"
	}
